Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Dietrich DFKI Bremen 2010
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerDominik.Dietrich@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CSL.ReduceProve

Description

Interface for Reduce CAS system.

Synopsis

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

getAxioms :: [Named CMD] -> ([Named CMD], [Named CMD]) Source #

splits a list of named sentences into axioms and sentences to be proven

isReduceAxiom :: Named CMD -> Bool Source #

checks whether a named sentence is a reduce axiom

reduceProve :: String -> Theory Sign CMD [EXPRESSION] -> a -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])]) Source #

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

connect to CAS, stepwise process the cmds

processCmdsIntern :: Session a => a -> [Named CMD] -> IO ([ProofStatus [EXPRESSION]], [(Named CMD, ProofStatus [EXPRESSION])]) Source #

internal function to process commands over an existing connection