Copyright | (c) Jonathan von Schroeder DFKI GmbH 2010 |
---|---|

License | GPLv2 or higher, see LICENSE.txt |

Maintainer | <jonathan.von_schroeder@dfki.de> |

Stability | experimental |

Portability | non-portable (imports Logic.Logic) |

Safe Haskell | Safe |

Sublogics for Propositional Logic

- slBasicSpec :: QBFSL -> BASICSPEC -> QBFSL
- data QBFFormulae
- data QBFSL = QBFSL {}
- sublogicsMax :: QBFSL -> QBFSL -> QBFSL
- top :: QBFSL
- bottom :: QBFSL
- sublogicsAll :: [QBFSL]
- sublogicsName :: QBFSL -> String
- slSig :: QBFSL -> Sign -> QBFSL
- slForm :: QBFSL -> FORMULA -> QBFSL
- slSym :: QBFSL -> Symbol -> QBFSL
- slSymit :: QBFSL -> SYMBITEMS -> QBFSL
- slMor :: QBFSL -> Morphism -> QBFSL
- slSymmap :: QBFSL -> SYMBMAPITEMS -> QBFSL
- prSymbolM :: QBFSL -> Symbol -> Maybe Symbol
- prSig :: QBFSL -> Sign -> Sign
- prMor :: QBFSL -> Morphism -> Morphism
- prSymMapM :: QBFSL -> SYMBMAPITEMS -> Maybe SYMBMAPITEMS
- prSymM :: QBFSL -> SYMBITEMS -> Maybe SYMBITEMS
- prFormulaM :: QBFSL -> FORMULA -> Maybe FORMULA
- prBasicSpec :: QBFSL -> BASICSPEC -> BASICSPEC
- isProp :: QBFSL -> Bool
- isHC :: QBFSL -> Bool

# Documentation

data QBFFormulae Source #

types of propositional formulae

Eq QBFFormulae Source # | |

Data QBFFormulae Source # | |

Ord QBFFormulae Source # | |

Show QBFFormulae Source # | |

sublogics for propositional logic

Eq QBFSL Source # | |

Data QBFSL Source # | |

Ord QBFSL Source # | |

Show QBFSL Source # | |

Logic QBF QBFSL BASICSPEC FORMULA SYMBITEMS SYMBMAPITEMS Sign Morphism Symbol Symbol ProofTree Source # | Instance of Logic for propositional logc |

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 Source # | |

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 Source # | |

sublogicsAll :: [QBFSL] Source #

all sublogics

sublogicsName :: QBFSL -> String Source #

prSymMapM :: QBFSL -> SYMBMAPITEMS -> Maybe SYMBMAPITEMS Source #