It represent An Atom of a clause as a Predicate (P) or as a equality (E)

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 (θ-subsumption): there is a substitution θ of the variables of the first clause such that every literal of c1θ is in c2. Only the variables of the first clause are instantiated, and c1 may not have more literals than c2 (so a clause does not subsume its own factors).

cfolSubsumes [ ( P ( "P", [] ) [ Var ( "X", [], 0 ) ], True ) ] [ ( P ( "P", [] ) [ Func ( "a", [] ) [] ], True ), ( P ( "Q", [] ) [], True ) ] == True

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.