Name: logic-classes Version: 1.4.1 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: http://src.seereason.com/logic-classes License: BSD3 Author: David Fox Maintainer: SeeReason Partners Bug-Reports: http://bugzilla.seereason.com/ Category: Logic, Theorem Provers Cabal-version: >= 1.9 Build-Type: Simple 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.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.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.Tests.HUnit 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 Build-Depends: applicative-extras, base >= 4.3 && < 5, containers, fgl, happstack-data, HUnit, incremental-sat-solver, mtl, syb-with-class, text, PropLogic, pretty, safecopy, set-extra, syb, template-haskell Executable tests GHC-Options: -Wall -O2 Main-Is: Data/Logic/Tests/Main.hs Build-Depends: applicative-extras, base, containers, happstack-data, HUnit, incremental-sat-solver, mtl, pretty, PropLogic, safecopy, set-extra, syb, template-haskell 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.Common Data.Logic.Tests.Harrison.Equal Data.Logic.Tests.Harrison.FOL 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