The module provides the tools for express formulas in their Clausal Form.
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.
It represent a set of ClauseFOL
It gives the variables that appears in a clause atom
It gives the variables that appears in a clause
It gives the symbol of the predicate of the atom ("=" is reserved for equality)
It gives the symbols of literals that appears in a clause
It applies a Substitution over a clause atom
It applies a substitution over a clause
It sorts the literals of the clause by alphabetical order.
It calculates the union of two clauses
Indicates if the first clause subsumes the second, that is, if the first is entirely contained in the second.
Indicates if the clause is a tautology, that is if it contains a literal and its complement.
Indicates if the clause is enterly positive, this is with all its literals positive
Indicates if the clause is enterly negative, this is with all its literals negative
It removes clauses that are equal from a list of clauses
It removes clauses that are tautological clauses
It removes clauses that are subsumed by other from the list
It converts a ClauseFOLAtom to an Atom (FormulaFOL)
It converts a ClauseFOLLiteral to a Literal (FormulaFOL)
It pass a CNF formula (opened) to a Set of clausses
Express a formula as a Set of clauses.
Express a set of formulas as a Set of clauses.
It reads the Cc 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.
It extracts the clause readed. If it is Nothing then it returns an empty clause
It gives the corresponding input syntax of a clause
It generates the String representation of a ClauseFOL using unicode symbols.
It generates the Latex string of a ClauseFOL. The result requires a math enviroment to be displayed.
It generates the String representation of a Set of Clauses using unicode symbols.
It generates the Latex string of a Set of Clauses. The result requires a math enviroment to be displayed.
It represent An Atom of a clause as a Predicate (P) or as a equality (E)