Copyright	(c) Otto-von-Guericke University of Magdeburg
License	GPLv2 or higher, see LICENSE.txt
Safe Haskell	None

HetsAPI.ProveCommands

Description

Synopsis

getTheoryForSelection :: [String] -> [String] -> [String] -> G_theory -> G_theory
getAvailableComorphisms :: G_theory -> [AnyComorphism]
getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
getUsableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)]
getUsableConservativityCheckers :: LEdge DGLinkLab -> LibEnv -> LibName -> IO [G_conservativity_checker]
proveNode :: TheoryPointer -> ProofOptions -> ResultT IO ProofResult
recordProofResult :: TheoryPointer -> ProofResult -> LibEnv
proveNodeAndRecord :: TheoryPointer -> ProofOptions -> ResultT IO (ProofResult, LibEnv)
checkConsistency :: TheoryPointer -> ConsCheckingOptions -> IO ConsistencyStatus
recordConsistencyResult :: TheoryPointer -> ConsistencyStatus -> LibEnv
checkConsistencyAndRecord :: TheoryPointer -> ConsCheckingOptions -> IO (ConsistencyStatus, LibEnv)
checkConservativityEdge :: LinkPointer -> G_conservativity_checker -> IO (Result ConservativityResult)
recordConservativityResult :: LinkPointer -> ConservativityResult -> LibEnv
checkConservativityEdgeAndRecord :: LinkPointer -> G_conservativity_checker -> IO (Result (ConservativityResult, LibEnv))
data ProofOptions = ProofOptions {
- proofOptsProver :: Maybe G_prover
- proofOptsComorphism :: Maybe AnyComorphism
- proofOptsUseTheorems :: Bool
- proofOptsGoalsToProve :: [String]
- proofOptsAxiomsToInclude :: [String]
- proofOptsTimeout :: Int
}
defaultProofOptions :: ProofOptions
data ConsCheckingOptions = ConsCheckingOptions {
- consOptsConsChecker :: Maybe G_cons_checker
- consOptsComorphism :: Maybe AnyComorphism
- consOptsIncludeTheorems :: Bool
- consOptsTimeout :: Int
}
defaultConsCheckingOptions :: ConsCheckingOptions
recomputeNode :: TheoryPointer -> LibEnv
genericProveBatch :: (Show sentence, Ord sentence, Ord proof_tree) => Bool -> Int -> [String] -> Bool -> Bool -> (Int -> Named sentence -> Maybe (Named sentence) -> (ATPRetval, GenericConfig proof_tree) -> IO Bool) -> (pst -> Named sentence -> pst) -> RunProver sentence proof_tree pst -> String -> String -> GenericState sentence proof_tree pst -> Maybe (MVar (Result [ProofStatus proof_tree])) -> IO [ProofStatus proof_tree]

Documentation

getTheoryForSelection :: [String] -> [String] -> [String] -> G_theory -> G_theory Source #

getAvailableComorphisms :: G_theory -> [AnyComorphism] Source #

getAvailableComorphisms theory yields all available comorphisms for theory

getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)] Source #

getUsableProvers theory checks for usable provers available on the machine

getUsableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)] Source #

getUsableConsistencyCheckers theory checks for usable consistencey checkers for theory available on the machine

getUsableConservativityCheckers :: LEdge DGLinkLab -> LibEnv -> LibName -> IO [G_conservativity_checker] Source #

proveNode :: TheoryPointer -> ProofOptions -> ResultT IO ProofResult Source #

proveNode theory prover comorphism proves all goals in theory using all all axioms in theory. If prover or comorphism is Nothing the first usable prover or comorphism, respectively, is used.

recordProofResult :: TheoryPointer -> ProofResult -> LibEnv Source #

proveNodeAndRecord :: TheoryPointer -> ProofOptions -> ResultT IO (ProofResult, LibEnv) Source #

checkConsistency :: TheoryPointer -> ConsCheckingOptions -> IO ConsistencyStatus Source #

recordConsistencyResult :: TheoryPointer -> ConsistencyStatus -> LibEnv Source #

checkConsistencyAndRecord :: TheoryPointer -> ConsCheckingOptions -> IO (ConsistencyStatus, LibEnv) Source #

checkConservativityEdge :: LinkPointer -> G_conservativity_checker -> IO (Result ConservativityResult) Source #

recordConservativityResult :: LinkPointer -> ConservativityResult -> LibEnv Source #

checkConservativityEdgeAndRecord :: LinkPointer -> G_conservativity_checker -> IO (Result (ConservativityResult, LibEnv)) Source #

data ProofOptions Source #

Constructors

ProofOptions

Fields

proofOptsProver :: Maybe G_prover
The prover to use. If not set, it is selected automatically
proofOptsComorphism :: Maybe AnyComorphism
The comorphism to use. If not set, it is selected automatically
proofOptsUseTheorems :: Bool
Indicates whether or not to use theorems is subsequent proofs
proofOptsGoalsToProve :: [String]
The names of the goals to prove. If empty, all goals are proven
proofOptsAxiomsToInclude :: [String]
The names of the axioms to include in the prove. If empty, all axioms are included
proofOptsTimeout :: Int
The timeout in seconds

defaultProofOptions :: ProofOptions Source #

data ConsCheckingOptions Source #

Constructors

ConsCheckingOptions
Fields consOptsConsChecker :: Maybe G_cons_checker The conschecker to use. If not set, it is selected automatically consOptsComorphism :: Maybe AnyComorphism The comorphism to use. If not set, it is selected automatically consOptsIncludeTheorems :: Bool Indicates whether or not to include theorems in the consistency check consOptsTimeout :: Int The timeout in seconds

defaultConsCheckingOptions :: ConsCheckingOptions Source #

recomputeNode :: TheoryPointer -> LibEnv Source #

genericProveBatch Source #

Arguments

:: (Show sentence, Ord sentence, Ord proof_tree)
=> Bool	True means use tLimit/options from GenericState
-> Int	batch time limit
-> [String]	extra options passed
-> Bool	True means include proved theorems
-> Bool
-> (Int -> Named sentence -> Maybe (Named sentence) -> (ATPRetval, GenericConfig proof_tree) -> IO Bool)	called after every prover run. return True if you want the prover to continue.
-> (pst -> Named sentence -> pst)	inserts a Namend sentence into a logicalPart
-> RunProver sentence proof_tree pst
-> String	prover name
-> String	theory name
-> GenericState sentence proof_tree pst
-> Maybe (MVar (Result [ProofStatus proof_tree]))	empty MVar to be filled after each proof attempt
-> IO [ProofStatus proof_tree]	proof status for each goal

A non-GUI batch mode prover. The list of goals is processed sequentially. Proved goals are inserted as axioms.