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

HetsAPI.ProveCommands

Description

Synopsis

getAvailableComorphisms :: G_theory -> [AnyComorphism]
getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
getUsableConsistencyCheckers :: G_theory -> IO [(G_cons_checker, AnyComorphism)]
proveNode :: G_theory -> 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)
checkConservativityNode :: LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory)
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

Documentation

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

proveNode :: G_theory -> 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 #

checkConservativityNode :: LNode DGNodeLab -> LibEnv -> LibName -> IO (String, LibEnv, ProofHistory) 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 #