Conjunctive normal form: represents a conjunction of clauses.

Represents a disjunction of literals.

Represents either a propositional variable or its negation, depending on whether the boolean second component is True or False, respectively.

Convert a Formula into conjunctive normal form.

Adapted from Figure 2.6 in

• Samuel Mimram (2020) PROGRAM = PROOF.

Convert a conjunctive normal form representation of a formula into a formula.

Convert a formula into a canonical conjunctive normal form.

Examples

>>> import AutoProof.Internal.Formula
>>> canonicalCNF $ Or (Not (Imp (Var "a") (Var "b"))) (Var "c")
And (Or (Var "c") (Not (Var "b"))) (Or (Var "c") (Var "a"))

Substitute a truth value for a variable in a CNF formula.

(substitute a x True) and (substitute a x False) represent the substitutions \(a[\top/x]\) and \(a[\bot/x]\), respectively.

Examples

>>> a = And (Imp (Var "a") (Not (And (Var "b") (Not (Var "c"))))) (Var "a")
>>> cnf = CNF.fromFormula a
>>> cnf
fromList [fromList [("a",False),("b",False),("c",True)],fromList [("a",True)]]
>>> cnf2 = CNF.substitute cnf "a" True
>>> cnf2
fromList [fromList [("b",False),("c",True)]]
>>> a2 = CNF.toFormula cnf2
>>> a2
Or (Var "c") (Not (Var "b"))

Substitute a truth value for a variable that occurs as a pure literal within a CNF formula with the same polarity as the truth value. This precondition is not checked.

Obtain the literal of a unitary clause of a CNF formula, if there is one.

A unitary clause is one in which exactly one literal occurs.

Obtain a pure literal of a CNF formula, if there is one.

A pure literal is one which only occurs with the a single polarity in the formula.

Obtain a literal from a CNF formula, if there is one.