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 cuantifier
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 cuantifiers 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 allows represent the Prenex Calculus Graph as DOT string, which could be rendered by GraphViz
It allows extract all the external cuantifiers, especially interesting for applying over Prenex Form Formulas
It gives the Skolem functions correspondence of a list of cuantifiers
It calculates the Skolem Form of a Formula
It calculates the Skolem Forms of the formulas of a set
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) cuantifier with the associated variable