| 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
- data PropProverState = PropProverState {}
- propProverState :: Sign -> [Named FORMULA] -> [FreeDefMorphism FORMULA Morphism] -> PropProverState
- insertSentence :: PropProverState -> Named FORMULA -> PropProverState
- transSenName :: String -> String
Documentation
data PropProverState
Datatype for the prover state for propositional logic
Constructors
| PropProverState | |
Fields
| |
Instances
Arguments
| :: Sign | |
| -> [Named FORMULA] | |
| -> [FreeDefMorphism FORMULA Morphism] | free definitions |
| -> PropProverState |
function to create prover state
transSenName :: String -> String
Translation of Sentence names