LogicUS.FOL

Design Goals

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.

Overview

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. (Future features: resolution strategies).

You can access to the installation guide, theoretical and practical contents, and more at LogicUS.