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 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 negations by applying De Morgan's laws where appropriate


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


f6 = fplInteriorizeAllNeg f4
f6 == Disj (Conj (Atom "p") (Conj (Atom "q") (Neg (Atom "r")))) (Conj (Disj (Neg (Atom "q")) (Atom "r")) (Neg (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 disjunctions 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"))))

Express a formula in its Negation Normal Form (NNF) that is formed only by literals and the conectives ∧ and/or ∨.


-- Check if f5 is in NNF
(f5 == fplToNNF f5) == True


-- Check if f1 is in NNF
(f1 == fplToNNF f1) == False


-- Calculate NNF form for f1
f9 = fplToNNF f1
f9 == Disj (Conj (Atom "p") (Conj (Atom "q") (Neg (Atom "r")))) (Conj (Disj (Neg (Atom "q")) (Atom "r")) (Neg (Atom "p")))


-- It is equal to f6
(f9 == f6) == True

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 represent a ClausePL as a list of literals.

c1 : ClausePL
c1 =
    [ Neg (Atom "p"), Neg (Atom "q"), Atom "r" ]


c2 : ClausePL
c2 =
    [ Neg (Atom "p"), Atom "r" ]


c3 : ClausePL
c3 =
    [ Atom "r" ]

It represent a List of ClausePL

cs : ClausePLSet
cs =
    [ c1, c2, c3 ]

Indicates if the clause is enterly positive, this is with all its literals positive

cplIsPositive c1 == False


cplIsPositive c3 == True

Indicates if the clause is enterly negative, this is with all its literals negative

cplIsNegative c1 == False


cplIsNegative (List.take 2 c1) == True

It checks if the clauses are equal, that is, if both have the same elements

(c1 == List.reverse c1) == False


cplEqClauses c1 (List.reverse c1) == True

Indicates if the first clause subsumes the second, that is, if the first is entirely contained in the second.

cplSubsumes c1 c2 == False


cplSubsumes c2 c1 == True

Indicates if the clause is a tautology, that is if it contains a literal and its complement.

cplIsTautology c1 == False


(cplIsTautology <| c1 ++ [ Atom "p" ]) == True

It removes clauses that are equal from a list of clauses

cs1 = [c1, c2, c3]


csplRemoveEqClauses c1 == c1


csplRemoveEqClauses (cs1 ++ (List.map (List.reverse) cs1)) == c1

It removes clauses that are tautological clauses

csplRemoveTautClauses <| List.map (\x -> x ++ [ Atom "q" ]) cs1 == [ [ Neg (Atom "p"), Atom "r", Atom "q" ], [ Atom "r", Atom "q" ] ]

It removes clauses that are subsumed by other from the list

csplRemoveSubsumedClauses cs1 == [ [ Atom "r" ] ]

It gives the propositional symbols that take place in the clause

cplSymbols c1 =
    [ "p", "q", "r" ]
cplSymbols c2 =
    [ "p", "r" ]
cplSymbols c3 =
    [ "r" ]

It gives the propositional symbols that take place in the clause

csplSymbols cs1 =
    [ "p", "q", "r" ]

It gives all possible interpretations for a clause

cplInterpretations c1 == [ [], [ "p" ], [ "p", "q" ], [ "p", "q", "r" ], [ "p", "r" ], [ "q" ], [ "q", "r" ], [ "r" ] ]


cplInterpretation c2 == [ [], [ "p" ], [ "p", "r" ], [ "r" ] ]

It gives all possible interpretations for a set of clauses

csplInterpretations cs1 == [ [], [ "p" ], [ "p", "q" ], [ "p", "q", "r" ], [ "p", "r" ], [ "q" ], [ "q", "r" ], [ "r" ] ]


csplInterpretations [ [ Atom "p" ], [ Atom "q" ] ] == [ [], [ "p" ], [ "p", "q" ], [ "q" ] ]

It evaluates the truth value of the clause regarding to a interpretation

cplValuation c2 [ "p", "r" ] == True


cplValuation c2 [] == True


cplValuation c2 [ "p" ] == False

It evaluates the truth value of a set of clauses regarding to a interpretation

csplValuation cs1 [ "r" ] == True


csplValuation cs1 [] == False

It generates all models of a clause by bruteforce, valuating the truth value for each interpretation

plModels c1 == [ [], [ "p" ], [ "p", "q", "r" ], [ "p", "r" ], [ "q" ], [ "q", "r" ], [ "r" ] ]


cplModels c2 == [ [], [ "p", "r" ], [ "r" ] ]


cplModels c3 == [ [ "r" ] ]

It generates all models of a set of clauses by bruteforce, valuating the truth value for each interpretation

csplModels cs1 == [ [ "p", "q", "r" ], [ "p", "r" ], [ "q", "r" ], [ "r" ] ]

It checks if a clause is unsatisfible, that is if it is empty.

cplIsInsat c1 == False


cplIsInsat c2 == False


cplIsInsat [] == True

It checks if a set of clauses is a tautology, that is if all clauses are tautologies.

csplIsTaut cs1 == False


csplIsTaut (List.map (\x -> x ++ [ Neg (Atom "r") ]) cs1) == True

It checks if a set of clauses is satisfiable by bruteforce, calculating its models and checking any exists

csplIsSat cs1 == True


csplIsSat (cs1 ++ [ Neg (Atom "r") ]) == False

It checks if a set of clauses are satisfiable by brute force, calculates its models and verifies that none exist.

Express a CNF formula as a Set of clauses. If input is not in CNF form Nothing is returned

fplToCNF f1 |> cplFromCNF == Just [ [ Atom "p" ], [ Neg (Atom "q") ], [ Atom "r" ], [ Neg (Atom "p") ], [ Atom "q" ], [ Neg (Atom "r") ] ]


fplToDNF f1 |> cplFromCNF == Nothing

Express a formula as a Set of clauses. fplToClauses f1 == [[Atom "p"],[Neg (Atom "q")],[Atom "r"],[Neg (Atom "p")],[Atom "q"],[Neg (Atom "r")]]

Express a set of formulas as a Set of clauses.

fs = List.map (fplReadExtraction << fplReadFromString) ["p->q", "p \\/ q -> r", "¬p \\/ q"]
cs = splToClauses fs
cs == [[Neg (Atom "p"),Atom "q"],[Neg (Atom "p"),Atom "r"],[Neg (Atom "q"),Atom "r"]]

It reads the formula from a string. It returns a tuple with may be a formula (if it can be read it) and a message of error it it cannot.

cplReadFromString "p_{1}, p_{2}, ¬q_{1}, q_{2}" == ( Just [ Atom "p_{1}", Atom "p_{2}", Neg (Atom "q_{1}"), Atom "q_{2}" ], "", "" )


cplReadFromString "{p_{1}, p_{2}, ¬q_{1}, q_{2}}" == ( Just [ Atom "p_{1}", Atom "p_{2}", Neg (Atom "q_{1}"), Atom "q_{2}" ], "", "" )


cplReadFromString "{p_{1}, p_{2}, ¬q_{1}, q_{2}" == ( Nothing, "{p_{1}, p_{2}, ¬q_{1}, q_{2}", "Error: [{ col = 29, problem = Expecting ',', row = 1 },{ col = 29, problem = Expecting '}', row = 1 }]" )


cplReadFromString "{p_{1}, p_{2}, ¬q_{1}, q_{2}" == ( Nothing, "{p_{1}, p_{2}, ¬q_{1}, q_{2}", "Error: [{ col = 29, problem = Expecting ',', row = 1 },{ col = 29, problem = Expecting '}', row = 1 }]" )


cplReadFromString "{}" == ( Just [], "", "" )


cplReadFromString "" == ( Nothing, "", "Argument is empty" )

It extracts the clause readed. If it is Nothing then it returns an empty clause

(cplReadExtraction << cplReadFromString) "p_{1}, p_{2}, ¬q_{1}, q_{2}" == [ Atom "p_{1}", Atom "p_{2}", Neg (Atom "q_{1}"), Atom "q_{2}" ]


(cplReadExtraction << cplReadFromString) "{p_{1}, p_{2}, ¬q_{1}, q_{2}" == []


(cplReadExtraction << cplReadFromString) "{}" == []

It gives the corresponding input syntax of a clause

cplToInputString c1 == "¬p,¬q,r"


cplToInputString c3 == "r"

It generates the String representation of a ClausePL using unicode symbols.

cplToString c1 == "{¬ p, ¬ q, r}"

It generates the Latex string of a ClausePL. The result requires a math enviroment to be displayed.

cplToMathString c1 == "\\left\\lbrace \\neg p, \\neg q, r\\right\\rbrace"

It generates the String representation of a Set of Clauses using unicode symbols.

csplToString cs == "{{¬ p, q},{¬ p, r},{¬ q, r}}"

It generates the Latex string of a Set of Clauses. The result requires a math enviroment to be displayed.

csplToMathString cs == "\\left\\lbrace\\left\\lbrace \\neg p, q\\right\\rbrace, \\, \\left\\lbrace \\neg p, r\\right\\rbrace, \\, \\left\\lbrace \\neg q, r\\right\\rbrace\\right\\rbrace"