The module provides the tools for expressing formulas in Prenex, Skolem, CNF, DNF.
It removes all the equivalences by changing it by the conjuction of the implications
It removes all the equivalences by changing it by the disjunction of the negation of the antecedent and the consecuent
It interiorizes negations applying the De Morgan Rule and the rule of negation of the quantifier
It interiorizes the disjunctions by applying distributive rule
It interiorizes the conjunctions by applying distributive rule
It transforms a FOL Formula into one equivalent Prenex Form
It transforms a FOL Formula into one equivalent Prenex Form. It gives the list of quantifiers and the open formula of the Prenex Form. It also gives a Graph with the Prenex form calculus
It indicates if a formula is in Prenex Form
It quantifies a formula with the quantifiers given by following the reverse order on applying it (tail to head)
It allows represent the Prenex Calculus Graph as DOT string, which could be rendered by GraphViz
It allows extract all the external quantifiers, especially interesting for applying over Prenex Form Formulas
It gives the Skolem functions correspondence of a list of quantifiers
It calculates the Skolem Form of a Formula, by prenexization plus the introduction of skolem functions
It calculates the Skolem Forms of the formulas of a set (by using ffolToSkolem2)
It calculates a negative normal form of a formula
It calculates a conjuctive normal form of a formula
It calculates a disjuntive normal form of a formula
It calculates negative normal forms of formulas of a set
It calculates conjuctive normal forms of formulas of a set
It calculates disjunctive normal forms of formulas of a set
It represents the universal (all) and existencial (exists) quantifier with the associated variable