It checks if the formula contains any equivalence as a part of it.


f1 = Neg (Equi (Atom "p") (Impl (Atom "q") (Atom "r")))
fplContainsEquiv f1 == True


f2 = Disj (Neg (Conj (Atom "p") (Conj (Atom "q") (Atom "r")))) (Disj (Conj (Atom "p") (Atom "q")) (Atom "r"))
fplContainsEquiv f2 == False

It checks if the formula contains any disjunction as a part of the formula


fplContainsDisj f1 == False


fplContainsDisj f2 == True

It checks if the formula contains any conjunction as a part of the formula

fplContainsConj f1 == False


fplContainsConj f2 == True

It eliminates all equivalences of a formula by replacing it with the conjunction of the corresponding implications.


f3 = fplRemoveAllEquiv f1
f3 == Neg (Conj (Impl (Atom "p") (Impl (Atom "q") (Atom "r"))) (Impl (Impl (Atom "q") (Atom "r")) (Atom "p")))

It checks if the formula contains any implication as a part of the formula


fplContainsImpl f1 == True


fplContainsImpl f2 == False

It eliminates all implications of a formula by replacing it with the conjunction of the corresponding implications.


f4 = fplRemoveAllImpl f3
f4 == Neg (Conj (Disj (Neg (Atom "p")) (Disj (Neg (Atom "q")) (Atom "r"))) (Disj (Neg (Disj (Neg (Atom "q")) (Atom "r"))) (Atom "p")))

It interiorizes the disjunctions by applying the AND Distributive law where appropriate.


f7 = fplInteriorizeAllDisj f6
f7 == Conj (Conj (Disj (Atom "p") (Disj (Neg (Atom "q")) (Atom "r"))) (Disj (Atom "p") (Neg (Atom "p")))) (Conj (Conj (Disj (Atom "q") (Disj (Neg (Atom "q")) (Atom "r"))) (Disj (Atom "q") (Neg (Atom "p")))) (Conj (Disj (Neg (Atom "r")) (Disj (Neg (Atom "q")) (Atom "r"))) (Disj (Neg (Atom "r")) (Neg (Atom "p")))))

It interiorizes the conjunctions by applying the OR Distributive law where appropriate.


f8 = fplInteriorizeAllConj f6
f8 == Disj (Conj (Atom "p") (Conj (Atom "q") (Neg (Atom "r")))) (Disj (Conj (Neg (Atom "q")) (Neg (Atom "p"))) (Conj (Atom "r") (Neg (Atom "p"))))

It interiorizes the negations by applying De Morgan's laws where appropriate


f5 = fpltoNNF f2
f5 == Disj (Disj (Neg (Atom "p")) (Disj (Neg (Atom "q")) (Neg (Atom "r")))) (Disj (Conj (Atom "p") (Atom "q")) (Atom "r"))


f6 = fplToNNF f4
f6 == Disj (Conj (Atom "p") (Conj (Atom "q") (Neg (Atom "r")))) (Conj (Disj (Neg (Atom "q")) (Atom "r")) (Neg (Atom "p")))

Express a formula in its Conjuction Normal Form (CNF) that is formed as a conjuction of disjuntive formulas.


 -- Check if f1 is in CNF
(f1 == fplToCNF f1) == False


-- Check if f7 is in CNF
(f7 == fplToCNF f7) == True


-- Calculate CNF for f1
f10 = fplToCNF f1
f10 == Conj (Conj (Disj (Atom "p") (Disj (Neg (Atom "q")) (Atom "r"))) (Disj (Atom "p") (Neg (Atom "p")))) (Conj (Conj (Disj (Atom "q") (Disj (Neg (Atom "q")) (Atom "r"))) (Disj (Atom "q") (Neg (Atom "p")))) (Conj (Disj (Neg (Atom "r")) (Disj (Neg (Atom "q")) (Atom "r"))) (Disj (Neg (Atom "r")) (Neg (Atom "p")))))


-- It is equal to f7
(f10 == f7) == True

Express a formula in its Disjunction Normal Form (CNF) that is formed as a conjuction of disjuntive formulas.


-- Check if f1 is in DNF
(f1 == fplToDNF f1) == False


-- Check if f8 is in DNF
(f8 == fplToCNF f8) == True


-- Calculate CNF for f1
f11 = fplToDNF f1
f11 == Disj (Conj (Atom "p") (Conj (Atom "q") (Neg (Atom "r")))) (Disj (Conj (Neg (Atom "q")) (Neg (Atom "p"))) (Conj (Atom "r") (Neg (Atom "p"))))


-- It is equal to f8
(f11 == f8) == True

It gives a formula in DNF as a list of literal sets. If the formula given is not in DNF it returns Nothing.

It gives a formula in CNF as a list of literal sets. If the formula given is not in CNF it returns Nothing.

It solves the satisfiability of a formula by its DNF

It gets the models by DNF of a formula

It solves the validity of a formula by its CNF.

It performs the Tseitin transformation of a formula (see splToCNFTseitin).

It performs the Tseitin transformation of a set of formulas. The result is a formula in CNF (at most three literals per clause) that is equisatisfiable with the set, not equivalent to it: each compound subformula gets a fresh symbol 𝜏ᵢ defined by an equivalence. Equal subformulas share their symbol, also across different formulas of the set, so the result grows linearly with the size of the set (the usual CNF may grow exponentially).

splToCNFTseitin [ fplRead "p & q -> r" ]
    == Conj (Conj (Conj (Conj (Disj (Neg (Atom ( "𝜏", [ 0 ] ))) (Disj (Neg (Atom ( "𝜏", [ 1 ] ))) (Atom ( "r", [] )))) ...

Deprecated: misspelled name kept for compatibility. Use fplToCNFTseitin.