It represent a literal of a clause as a tuple with the symbol of the literal (string) and the sign of the literal (False:negative literal, True:positive literal).

It represent a set of clause literals.

c1 : ClausePL
c1 =
    [ ( "p", False ), ( "q", False ), ( "r", True ) ]


c2 : ClausePL
c2 =
    [ ( "p", False ), ( "r", True ) ]


c3 : ClausePL
c3 =
    [ ( "r", True ) ]

It represent a set of ClausePL

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

It sorts the literals of the clause by alphabetical order.

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

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 ++ [ ( "p", True ) ]) == True

It removes clauses that are equal from a list of clauses

cs1 = [c1, c2, c3]


csplRemoveEqClauses cs1 == cs1


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

It removes clauses that are tautological clauses

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

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", True ) ] ]

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 ++ [ ( "r", False ) ]) 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 ++ [ ( "r", False ) ]) == False

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

It converts a ClausePLLiteral to a Literal (FormulaPL)

It pass a CNF formula to a Set of clausses

Express a formula as a Set of clauses.

f1 = (fplReadExtraction << fplReadFromString) "¬p & q <-> r"
fplToClauses f1 == [[("p",True),("q",False),("r",True)],[("p",False),("r",False)],[("q",True),("r",False)]]

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 == [[("p",False),("q",True)],[("p",False),("r",True)],[("q",False),("r",True)]]

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 [("p_{1}",True),("p_{2}",True),("q_{1}",False),("q_{2}",True)],"","")


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


cplReadFromString "{p_{1}, p_{2}, ¬q_{1}, q_{2}" == (Nothing,"{p_{1},p_{2},¬q_{1},q_{2}","Error: [{ col = 26, problem = Expecting ',', row = 1 },{ col = 26, 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}" == [ ( "p_{1}", True ), ( "p_{2}", True ), ( "q_{1}", False ), ( "q_{2}", True ) ]


(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"