Name: logic-classes
Version: 0.44
License: BSD3
Author: David Fox <dsf@seereason.com>
Maintainer: SeeReason Partners <partners@seereason.com>
Synopsis: Symbolic logic support - a class framework, example instances, polymorphic implementations
Description: 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.
Build-Type: Custom
Category: Logic, Theorem Provers
Cabal-version: >= 1.2
Library
GHC-options: -threaded -Wall -O2
Exposed-Modules: Data.Logic
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
Data.Logic.Instances.Chiou
Data.Logic.Instances.PropLogic
Data.Logic.Instances.SatSolver
Data.Logic.KnowledgeBase
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
Data.Logic.Types.FirstOrder
Data.Logic.Types.FirstOrderPublic
Data.Logic.Types.Propositional
Other-Modules: Data.Logic.Test
Build-Depends: base < 5, containers, fgl, happstack-data, incremental-sat-solver,
mtl, syb-with-class, text, PropLogic, pretty, safecopy, set-extra, syb
Executable tests
Main-Is: Test/Test.hs
Build-Depends: HUnit