Unavailable. Nobody can download this version any more, with elm or with the Lamdera compiler: github.com/vicramgon/logicus is gone (deleted or private); Software Heritage not asked yet (this run's --swh-calls were used up); no fork with tag 8.0.2 found (12 same-name repos checked); no cached copy. Use another version.
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 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 represents the universal (all) and existencial (exists) cuantifier with the associated variable