| Copyright | (c) Dominik Luecke Uni Bremen 2007 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | luecke@informatik.uni-bremen.de |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
Propositional.ProverState
Description
Prover state for propositional logic
Synopsis
- data PropProverState = PropProverState {}
- propProverState :: Sign -> [Named FORMULA] -> [FreeDefMorphism FORMULA Morphism] -> PropProverState
- insertSentence :: PropProverState -> Named FORMULA -> PropProverState
- transSenName :: String -> String
Documentation
data PropProverState Source #
Datatype for the prover state for propositional logic
Constructors
| PropProverState | |
Fields
| |
Instances
| Show PropProverState Source # | |
Defined in Propositional.ProverState Methods showsPrec :: Int -> PropProverState -> ShowS show :: PropProverState -> String showList :: [PropProverState] -> ShowS | |
Arguments
| :: Sign | |
| -> [Named FORMULA] | |
| -> [FreeDefMorphism FORMULA Morphism] | free definitions |
| -> PropProverState |
function to create prover state
transSenName :: String -> String Source #
Translation of Sentence names