The logic-classes package

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.

Properties

Versions	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
Dependencies	applicative-extras, base (≥4.3 & <5), containers, fgl, HUnit, incremental-sat-solver, mtl, pretty, PropLogic (≥0.9.0.3), safecopy, set-extra, syb, syb-with-class, template-haskell, text
License	BSD3
Author	David Fox <dsf@seereason.com>
Maintainer	SeeReason Partners <partners@seereason.com>
Category	Logic, Theorem Provers
Home page	http://src.seereason.com/logic-classes
Bug tracker	http://bugzilla.seereason.com/
Executables	tests
Upload date	Wed Apr 18 14:30:53 UTC 2012
Uploaded by	DavidFox
Build failure	ghc-7.4 (log)

Modules

Data
- Logic
  - Classes
    - Data.Logic.Classes.Apply
    - Data.Logic.Classes.Arity
    - Data.Logic.Classes.Atom
    - Data.Logic.Classes.ClauseNormalForm
    - Data.Logic.Classes.Combine
    - Data.Logic.Classes.Constants
    - Data.Logic.Classes.Equals
    - Data.Logic.Classes.FirstOrder
    - Data.Logic.Classes.Formula
    - Data.Logic.Classes.Literal
    - Data.Logic.Classes.Negate
    - Data.Logic.Classes.Pretty
    - Data.Logic.Classes.Propositional
    - Data.Logic.Classes.Skolem
    - Data.Logic.Classes.Term
    - Data.Logic.Classes.Variable
  - Harrison
    - Data.Logic.Harrison.DP
    - Data.Logic.Harrison.DefCNF
    - Data.Logic.Harrison.Equal
    - Data.Logic.Harrison.FOL
    - Formulas
      - Data.Logic.Harrison.Formulas.FirstOrder
      - Data.Logic.Harrison.Formulas.Propositional
    - Data.Logic.Harrison.Herbrand
    - Data.Logic.Harrison.Lib
    - Data.Logic.Harrison.Meson
    - Data.Logic.Harrison.Normal
    - Data.Logic.Harrison.Prolog
    - Data.Logic.Harrison.Prop
    - Data.Logic.Harrison.PropExamples
    - Data.Logic.Harrison.Resolution
    - Data.Logic.Harrison.Skolem
    - Data.Logic.Harrison.Tableaux
    - Data.Logic.Harrison.Unif
  - 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.Resolution
  - Data.Logic.Satisfiable
  - Tests
    - Data.Logic.Tests.HUnit
  - Types
    - Data.Logic.Types.Common
    - Data.Logic.Types.FirstOrder
    - Data.Logic.Types.FirstOrderPublic
    - Harrison
      - Data.Logic.Types.Harrison.Equal
      - Data.Logic.Types.Harrison.FOL
      - Formulas
        Data.Logic.Types.Harrison.Formulas.FirstOrder
        Data.Logic.Types.Harrison.Formulas.Propositional
      - Data.Logic.Types.Harrison.Prop
    - Data.Logic.Types.Propositional

Downloads

logic-classes-1.4.5.tar.gz (Cabal source package)
package description (included in the package)