| Copyright | (c) Dominik Dietrich, DFKI Bremen, 2010 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Dominik.Dietrich@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CSL.ReduceProve
Description
Interface for Reduce CAS system.
- mkProverTemplateWithLemmaExport :: String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO ([ProofStatus proof_tree], [(Named sentence, ProofStatus proof_tree)])) -> ProverTemplate theory sentence morphism sublogics proof_tree
- reduceProver :: Prover Sign CMD Morphism () [EXPRESSION]
- getAxioms :: [Named CMD] -> ([Named CMD], [Named CMD])
- isReduceAxiom :: Named CMD -> Bool
- reduceProve :: String -> Theory Sign CMD [EXPRESSION] -> a -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
- processCmds :: [Named CMD] -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
- processCmdsIntern :: Session a => a -> [Named CMD] -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
Documentation
mkProverTemplateWithLemmaExport :: String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO ([ProofStatus proof_tree], [(Named sentence, ProofStatus proof_tree)])) -> ProverTemplate theory sentence morphism sublogics proof_tree
reduceProver :: Prover Sign CMD Morphism () [EXPRESSION]
the prover
getAxioms :: [Named CMD] -> ([Named CMD], [Named CMD])
splits a list of named sentences into axioms and sentences to be proven
isReduceAxiom :: Named CMD -> Bool
checks whether a named sentence is a reduce axiom
reduceProve :: String -> Theory Sign CMD [EXPRESSION] -> a -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
takes a theory name and a theory as input, starts the prover and returns a list of ProofStatus.
processCmds :: [Named CMD] -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
connect to CAS, stepwise process the cmds
processCmdsIntern :: Session a => a -> [Named CMD] -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])])
internal function to process commands over an existing connection