logic-classes: Support for propositional and first order logic, normal forms, and a resolution theorem prover.

[ bsd3, library, logic, theorem-provers ] [ Propose Tags ] [ Report a vulnerability ]

Package to support Propositional and First Order Logic. It includes classes representing the different types of formulas and terms, some instances of those classes for types used in other logic libraries, and implementations of several logic algorithms, including conversion to normal form and a simple resolution-based theorem prover for any instance of FirstOrderFormula.

Modules

[Last Documentation]

Data
- Data.Logic
  - Classes
    - Data.Logic.Classes.Arity
    - Data.Logic.Classes.Boolean
    - Data.Logic.Classes.ClauseNormalForm
    - Data.Logic.Classes.FirstOrder
    - Data.Logic.Classes.Literal
    - Data.Logic.Classes.Logic
    - Data.Logic.Classes.Negatable
    - Data.Logic.Classes.Pred
    - Data.Logic.Classes.Propositional
    - Data.Logic.Classes.Skolem
    - Data.Logic.Classes.Term
    - Data.Logic.Classes.Variable
  - Instances
    - Data.Logic.Instances.Chiou
    - Data.Logic.Instances.PropLogic
    - Data.Logic.Instances.SatSolver
  - Data.Logic.KnowledgeBase
  - Normal
    - Data.Logic.Normal.Clause
    - Data.Logic.Normal.Implicative
    - Data.Logic.Normal.Negation
    - Data.Logic.Normal.Prenex
    - Data.Logic.Normal.Skolem
  - Data.Logic.Resolution
  - Data.Logic.Satisfiable
  - Types
    - Data.Logic.Types.FirstOrder
    - Data.Logic.Types.FirstOrderPublic
    - Data.Logic.Types.Propositional

Downloads

logic-classes-0.47.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

DavidFox

For package maintainers and hackage trustees

edit package information

Candidates

No Candidates

Versions [RSS]	0.44, 0.45, 0.47, 0.48, 1.1, 1.4, 1.4.1, 1.4.2, 1.4.3, 1.4.4, 1.4.5, 1.4.6, 1.4.7, 1.4.8, 1.5, 1.5.1, 1.5.2, 1.5.3, 1.7, 1.7.1
Dependencies	base (>=4.3 && <5), containers, fgl, happstack-data, HUnit, incremental-sat-solver, mtl, pretty, PropLogic, safecopy, set-extra, syb, syb-with-class, text [details]
License	BSD-3-Clause
Author	David Fox <dsf@seereason.com>
Maintainer	SeeReason Partners <partners@seereason.com>
Category	Logic, Theorem Provers
Uploaded	by DavidFox at 2011-12-02T19:49:10Z
Distributions
Reverse Dependencies	1 direct, 0 indirect [details]
Executables	tests
Downloads	13571 total (5 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs not available [build log] All reported builds failed as of 2016-12-26 [all 7 reports]