CnfConverter¶

@ brief convert a generic propositional formula to CNF (conjunction of disjunctions of literals).

Propositional formulae are of the form:

• V: a proposition may be represented as a variable or as a Prolog atom

• 0, 1: false and true

• A*B -> the conjunction of two formulae

• A+B -> the disjunction of two formulae

• -A -> the negation of a formula

• A xor B: the exclusive-or of two formulae

• A == B: the logical equivalence of two formulae

• A -> B: the logical implication of two formulae

The output of the converter is a list of lists. The external list represents a conjunction. The internal lists represent a disjunction, or clause. Clauses disjoin propositions, or positive literals, and negated propositions, or negative literals.

The converter adds an extra variable F to represent the truth value of the formula.

• cnf/3
• prolog::cnf_dl/2
• prolog::cnf/2

Functions:¶

1. prolog::cnf_2::cnf/2(int ARG1, int ARG2)():

1. prolog::cnf_dl_2::cnf_dl/2(int ARG1, int ARG2)():