Name:             logic-classes
Version:          1.1
License:          BSD3
Author:           David Fox <dsf@seereason.com>
Maintainer:       SeeReason Partners <partners@seereason.com>
Synopsis:         Support for propositional and first order logic, normal forms, and a resolution theorem prover.
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: -Wall -O2
 Exposed-Modules:  Data.Logic.Classes.Arity
                   Data.Logic.Classes.Apply
                   Data.Logic.Classes.ClauseNormalForm
                   Data.Logic.Classes.Combine
                   Data.Logic.Classes.Constants
                   Data.Logic.Classes.Equals
                   Data.Logic.Classes.FirstOrder
                   Data.Logic.Classes.Literal
                   Data.Logic.Classes.Negate
                   Data.Logic.Classes.Propositional
                   Data.Logic.Classes.Skolem
                   Data.Logic.Classes.Term
                   Data.Logic.Classes.Variable
                   Data.Logic.Harrison.Equal
                   Data.Logic.Harrison.FOL
                   Data.Logic.Harrison.Formulas.FirstOrder
                   Data.Logic.Harrison.Formulas.Propositional
                   Data.Logic.Harrison.Lib
                   Data.Logic.Harrison.Meson
                   Data.Logic.Harrison.Normal
                   Data.Logic.Harrison.Prolog
                   Data.Logic.Harrison.Prop
                   Data.Logic.Harrison.Resolution
                   Data.Logic.Harrison.Skolem
                   Data.Logic.Harrison.Tableaux
                   Data.Logic.Harrison.Unif
                   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.Resolution
                   Data.Logic.Satisfiable
                   Data.Logic.Types.FirstOrder
                   Data.Logic.Types.FirstOrderPublic
                   Data.Logic.Types.Harrison.Equal
                   Data.Logic.Types.Harrison.FOL
                   Data.Logic.Types.Harrison.Formulas.FirstOrder
                   Data.Logic.Types.Harrison.Formulas.Propositional
                   Data.Logic.Types.Harrison.Prop
                   Data.Logic.Types.Propositional
 Build-Depends:    applicative-extras, base >= 4.3 && < 5, containers, fgl, happstack-data, incremental-sat-solver,
                   mtl, syb-with-class, text, PropLogic, pretty, safecopy, set-extra, syb

Executable tests
 GHC-Options: -Wall -O2
 Main-Is: Data/Logic/Tests/Main.hs
 Build-Depends: HUnit
 Other-Modules:    Data.Logic.Tests.Chiou0
                   Data.Logic.Tests.Common
                   Data.Logic.Tests.Data
                   Data.Logic.Tests.Logic
                   Data.Logic.Tests.TPTP
                   Data.Logic.Tests.Harrison.Equal
                   Data.Logic.Tests.Harrison.FOL
                   Data.Logic.Tests.Harrison.HUnit
                   Data.Logic.Tests.Harrison.Meson
                   Data.Logic.Tests.Harrison.Prop
                   Data.Logic.Tests.Harrison.Resolution
                   Data.Logic.Tests.Harrison.Skolem
                   Data.Logic.Tests.Harrison.Main
                   Data.Logic.Tests.Harrison.Unif