This package has been created to work with computer logic, specifically with First Order Logic. For a series of types and functions have been created that allow the definition and interpretation of formulas as well as the application of the main algorithms to reduce the consistency of formulas and sets.
The LogicUS.FOL packages allow working with formulas and sets in First Order Logic. It includes aspects like L-Structures valuation, substitution performing, normal forms, clauses and other algorithms like Semantic Tableaux, Herbrand Works or Resolution. Next, we make a synopsis of each of the modules exposed:
LogicUS.FOL.SintaxSemantics: It constitutes the basis of first logic, so that it exposes the syntax for the definition of the formulas and substituions (including all the operations with it, like clausre, variable renaming, ...) as well as the semantics for the L-Structure and its evaluation.
LogicUS.FOL.SemanticTableaux: It develops all the necessary tools for working with semantic boards in FOL, distinguishing the different types of formulas and rules and also allowing the visualization of the complete board.
LogicUS.FOL.NormalForms: It contains the functions necessary for the transformation of formulas into normal forms: Prenex, Skolem, NNF, CNF, DNF.
LogicUS.FOL.Clauses: It provides some functions that allow work with first order clauses, definition, operations, transformation of formulas and sets into clausal sets, ...
LogicUS.FOL.Herbrand: It defines the functions necessary for the application of the Herbrand Works (Universe, interpretations, models, ...)
LogicUS.FOL.Unification: It provides the functions for working with the unification algorithms: terms and atoms MGU.
LogicUS.FOL.Resolution: It gives the functions for working with the resolution algorithm in FOL and its representation, with several strategies (shortest clause first, linear, positive, negative).
LogicUS.FOL.SemanticTableauxEQ: Semantic tableaux for first order logic with equality.
LogicUS.FOL.SemanticTableauxFV: Semantic tableaux with free variables: the universal formulas are instantiated with new variables, which get their values by unification when a branch is closed, and the search backtracks over the ways of closing the branches. It finds closed tableaux that the ground tableaux of SemanticTableaux only find with the right terms, and the tree shows each variable and the substitution that closes each branch.
LogicUS.FOL.Prover9Mace4 and LogicUS.FOL.TPTP: For problems too big for the didactic algorithms, they translate a problem to the input of external provers (Prover9 and Mace4, and any prover that reads TPTP, such as E) and read their answers back. Mace4 models are returned as L-structures, so they can be checked and shown with the rest of the library. Running the provers is up to the application.
tests/ contains semantic tests that compare the algorithms with a reference implementation on small finite structures. Run them with npx elm-test.
You can access to the installation guide, theoretical and practical contents, and more at LogicUS.