logic-classes: Support for propositional and first order logic, normal forms, and a resolution theorem prover.

[ bsd3, library, logic, theorem-provers ] [ Propose Tags ]

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.

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, 1.4.8, 1.5, 1.5.1, 1.5.2, 1.5.3, 1.7, 1.7.1
Dependencies base (<5), containers, fgl, happstack-data, HUnit, incremental-sat-solver, mtl, pretty, PropLogic, safecopy, set-extra, syb, syb-with-class, text [details]
License BSD-3-Clause
Author David Fox <dsf@seereason.com>
Maintainer SeeReason Partners <partners@seereason.com>
Category Logic, Theorem Provers
Uploaded by DavidFox at Fri Oct 14 20:04:09 UTC 2011
Distributions NixOS:1.7.1
Executables tests
Downloads 5927 total (16 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-26 [all 7 reports]
Hackage Matrix CI

Modules

  • Data
    • Data.Logic
      • Classes
        • 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
      • 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.Normal.Negation
        • Data.Logic.Normal.Prenex
        • Data.Logic.Normal.Skolem
      • Data.Logic.Resolution
      • Data.Logic.Satisfiable
      • Types
        • Data.Logic.Types.FirstOrder
        • Data.Logic.Types.FirstOrderPublic
        • Data.Logic.Types.Propositional

Downloads

Maintainer's Corner

For package maintainers and hackage trustees