vicramgon/logicus

Elm packages for working with Propositional and First Order Logic algorithms.


License
BSD-3-Clause
Install
elm-package install vicramgon/logicus 5.0.0

Documentation

LogicUS

Design Goals

This package has been created to work with computer logic, specifically with propositional logic and first-order logic (in development). 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

Modules designed provides the tools that allow the definition, execution and visualization of main algorithms in the regarding area. In concrete:

Propositional Logic

The LogicUS.PL packages allow the definition of formulas and propositional sets on which a series of also implemented solving algorithms can be applied. Next, we make a synopsis of each of the modules exposed:

  • LogicUS.PL.SintaxSemantics: It constitutes the basis of propositional logic, so that it exposes the syntax for the definition of the formulas as well as the semantics for their interpretation as well as some basic algorithm in the field of propositional logic.

  • LogicUS.PL.SemanticTableaux: It develops all the necessary tools for working with semantic boards in PL, distinguishing the different types of formulas and rules and also allowing the visualization of the complete board.

  • LogicUS.PL.NormalForms: It contains the functions necessary for the transformation of formulas into normal forms (negative, conjunctive and disjunctive).

  • LogicUS.PL.Clauses: It provides some functions that allow work with propositional clauses, definition, operations, transformation of formulas and sets into clausal sets, ...

  • LogicUS.PL.DPLL: It defines the functions necessary for the application of the DPLL solving algorithm to sets of propositional clauses as well as the search for models, based on this technique. Also, it allows the visualization of the complete board.

  • LogicUS.PL.CSP: It defines the functions necessary for working with BigFormulas including its definition and a basic SAT Solver (based in Backtracking + MRV) for solving some (little) CSP.

  • LogicUS.PL.Resolution: Define the functions for working with the resolution algorithms implementing different strategies: saturation, regular, best first, linear, positive, negative, unitary, by inputs, ...

First Order Logic

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: Define the functions for working with the unification algorithms: terms and atoms MGU.

  • LogicUS.FOL.Resolution: Define the functions for working with the resolution algorithm in FOL and its representation. (Future features: resolution strategies).