Name:             logic-classes
Version:          1.5.3
Synopsis:         Framework for propositional and first order logic, theorem proving
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.
Homepage:         https://github.com/seereason/logic-classes
License:          BSD3
License-File:     COPYING
Author:           David Fox <dsf@seereason.com>
Maintainer:       SeeReason Partners <partners@seereason.com>
Bug-Reports:      https://github.com/seereason/logic-classes/issues
Category:         Logic, Theorem Provers
Cabal-version:    >= 1.9
Build-Type:       Simple
Extra-Source-Files: changelog

Library
 GHC-options: -Wall -O2
 Exposed-Modules:  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
                   Data.Logic.Failing
                   Data.Logic.Harrison.DefCNF
                   Data.Logic.Harrison.DP
                   Data.Logic.Harrison.Equal
                   Data.Logic.Harrison.FOL
                   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
                   Data.Logic.HUnit
                   Data.Logic.Instances.Chiou
                   Data.Logic.Instances.PropLogic
                   Data.Logic.Instances.SatSolver
                   -- Data.Logic.Instances.TPTP
                   Data.Logic.KnowledgeBase
                   Data.Logic.Normal.Clause
                   Data.Logic.Normal.Implicative
                   Data.Logic.Resolution
                   Data.Logic.Satisfiable
                   Data.Logic.Types.Common
                   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
                   Data.Boolean
                   Data.Boolean.SatSolver
 Build-Depends:    applicative-extras, base >= 4.3 && < 5, containers, HUnit, mtl, pretty, PropLogic, safecopy, set-extra, syb, template-haskell

Test-Suite logic-classes-tests
 Type: exitcode-stdio-1.0
 GHC-Options: -Wall -O2
 Hs-Source-Dirs: Data/Logic/Tests
 Main-Is: Main.hs
 Build-Depends: applicative-extras, base, containers, HUnit, logic-classes, mtl, pretty, PropLogic, set-extra, syb