Copyright | (c) Jonathan von Schroeder, DFKI GmbH 2010 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | <jonathan.von_schroeder@dfki.de> |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Definition of abstract syntax for propositional logic extended with QBFs
Ref. http://en.wikipedia.org/wiki/Propositional_logic http://www.voronkov.com/lics.cgi
- data FORMULA
- data BASICITEMS
- newtype BASICSPEC = BasicSpec [Annoted BASICITEMS]
- data SYMBITEMS = SymbItems [SYMB] Range
- newtype SYMB = SymbId Token
- data SYMBMAPITEMS = SymbMapItems [SYMBORMAP] Range
- data SYMBORMAP
- data PREDITEM = PredItem [Token] Range
- isPrimForm :: FORMULA -> Bool
- data ID = ID Token (Maybe Token)
Documentation
data FORMULA
Datatype for QBF formulas
Eq FORMULA | |
Data FORMULA | |
Ord FORMULA | |
Show FORMULA | |
ShATermConvertible FORMULA | |
GetRange FORMULA | |
Pretty FORMULA | |
Typeable * FORMULA | |
ProjectSublogicM QBFSL FORMULA | |
MinSublogic QBFSL FORMULA | |
Sentences QBF FORMULA Sign Morphism Symbol | Instance of Sentences for propositional logic |
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol | Static Analysis for propositional logic |
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree | Instance of Logic for propositional logc |
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree | |
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree |
data BASICITEMS
newtype BASICSPEC
Data BASICSPEC | |
Show BASICSPEC | |
ShATermConvertible BASICSPEC | |
Monoid BASICSPEC | |
GetRange BASICSPEC | |
Pretty BASICSPEC | |
Typeable * BASICSPEC | |
ProjectSublogic QBFSL BASICSPEC | |
MinSublogic QBFSL BASICSPEC | |
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS | Syntax of Propositional logic |
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol | Static Analysis for propositional logic |
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree | Instance of Logic for propositional logc |
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree | |
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree |
data SYMBITEMS
Eq SYMBITEMS | |
Data SYMBITEMS | |
Ord SYMBITEMS | |
Show SYMBITEMS | |
ShATermConvertible SYMBITEMS | |
GetRange SYMBITEMS | |
Pretty SYMBITEMS | |
Typeable * SYMBITEMS | |
ProjectSublogicM QBFSL SYMBITEMS | |
MinSublogic QBFSL SYMBITEMS | |
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS | Syntax of Propositional logic |
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol | Static Analysis for propositional logic |
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree | Instance of Logic for propositional logc |
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree | |
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree |
newtype SYMB
data SYMBMAPITEMS
Eq SYMBMAPITEMS | |
Data SYMBMAPITEMS | |
Ord SYMBMAPITEMS | |
Show SYMBMAPITEMS | |
ShATermConvertible SYMBMAPITEMS | |
GetRange SYMBMAPITEMS | |
Pretty SYMBMAPITEMS | |
Typeable * SYMBMAPITEMS | |
ProjectSublogicM QBFSL SYMBMAPITEMS | |
MinSublogic QBFSL SYMBMAPITEMS | |
Syntax QBF BASICSPEC Symbol SYMBITEMS SYMBMAPITEMS | Syntax of Propositional logic |
StaticAnalysis QBF BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol | Static Analysis for propositional logic |
Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree | Instance of Logic for propositional logc |
Comorphism QBF2Prop QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree | |
Comorphism Prop2QBF Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree |
data SYMBORMAP
data PREDITEM
predicates = propositions
isPrimForm :: FORMULA -> Bool