Yet More About ClausesReally Advanced Topics
To the solver reading clauses, any formula whose main operator is a connective or a quantifier is just another atom. This is in keeping with the solver’s treatment of our logical language, in which bool is just another sort whose domain is fixed as the two truth values FALSE and TRUE, so connectives are just predicates over bool. Hence, for example, AND is simply a function symbol like + except that its arguments and value are of sort bool rather than int.
However, it is useful to be able to simplify the problem input by removing the main logical operator of an atom. This also removes the need to reason about the meaning of that operator during the search for models. To pursue the example, if a formula A AND B occurs as one of the antecedent atoms to the left of the arrow in a clause, it can equivalently be replaced by A , B. If it occurs as a consequent atom, to the right of the arrow, the whole clause can equivalently be replaced by two clauses, one with A in that position and the other with B.
The full list of reductions is given below. Since the order of the antecedents of a clause is irrelevant, we can assume without loss of generality that the atom to be reduced is the last one before the arrow. Similarly, the consequents are also essentially unordered, so we can shuffle them to get the one to be reduced to be the first after the arrow. This is just to simplify the table—-it has no logical significance. To simplify even more, let A and C stand for A 1 , … , A m and C 1 ; … ; C n respectively.
| Clause | Reduces to | ||
| ∧ on the left | A , X ∧ Y -> C | A , X , Y -> C | replace ∧ by comma |
| ∧ on the right | A -> X ∧ Y ; C | A -> X ; C A -> Y ; C |
split into 2 clauses |
| ∨ on the left | A , X ∨ Y -> C | A , X -> C A , Y -> C |
split into 2 clauses |
| ∨ on the right | A -> X ∨ Y ; C | A -> X ; Y ; C | replace ∨ by semicolon |
| ¬ on the left | A , ¬X -> C | A -> X ; C | remove ¬ and flip sides |
| ¬ on the right | A -> ¬X ; C | A , X -> C | remove ¬ and flip sides |
| → on the left | A , X → Y -> C | A -> X ; C A , Y -> C |
treat X → Y as ¬X ∨ Y |
| → on the right | A -> X → Y ; C | A , X -> Y ; C | treat X → Y as ¬X ∨ Y |
| ∀ on the left | A , ∀vX -> C | A , sk(v,X) -> C | skolemise |
| ∀ on the right | A -> ∀vX ; C | A -> X ; C | delete the quantifier |
| ∃ on the left | A , ∃vX -> C | A , X -> C | delete the quantifier |
| ∃ on the right | A -> ∃vX ; C | A -> sk(v,X) ; C | skolemise |
Where x 1, …, x k are the free variables in a clause and v is a bound variable and X a formula, sk(v,X) in that clause is the result of substituting the term f ( x 1, …, x k ) for all occurrences of v in X, where f is a k-ary function symbol new to the context.
Clearly, by repeating these reductions until no more moves are possible, all occurrences of connectives and quantifiers may be removed from any clause. The result is in general not quite equivalent to the original, since skolemisation does not preserve equivalence, but it has models if and only if the original has models.
There is a little more to it, however. Following the above naive rules could lead to a large increase in the size of the formula, as A and C get duplicated in some cases. Where this threatens to happen, new function symbols (similar to skolem functions) are introduced to stand in for certain formulae, so that duplication is limited to atoms and exponential blowup is avoided. For the purposes of using this site, you do not generally need to know about this machinery behind the scenes, but in case you are interested you can start here.