| 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 |
QBF.AS_BASIC_QBF
Description
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
Constructors
Instances
| 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
Constructors
| PredDecl PREDITEM | |
| AxiomItems [Annoted FORMULA] |
newtype BASICSPEC
Constructors
| BasicSpec [Annoted BASICITEMS] |
Instances
| 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
Instances
| 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
Constructors
| SymbMapItems [SYMBORMAP] Range |
Instances
| 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