(* Title: Clausal Logic Author: Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017 Author: Dmitriy Traytel <traytel at inf.ethz.ch>, 2014 Author: Mathias Fleury <mathias.fleury at mpi-inf.mpg.de>, 2014 Maintainer: Jasmin Blanchette <jasmin.blanchette at inria.fr> *) section ‹Clausal Logic› theory Clausal_Logic imports Nested_Multisets_Ordinals.Multiset_More begin text ‹ Resolution operates of clauses, which are disjunctions of literals. The material formalized here corresponds roughly to Sections 2.1 (``Formulas and Clauses'') of Bachmair and Ganzinger, excluding the formula and term syntax. › subsection ‹Literals› text ‹ Literals consist of a polarity (positive or negative) and an atom, of type @{typ 'a}. ›