hets -- a heterogenous Specification (CASL) tool setContentsIndex
Logic.Prover
Portability portable
Stability provisional
Maintainer hets@tzi.de
Description
Provide prover stuff for class Logic.Sentences
Synopsis
data Theory sign sen = Theory {
sign_of :: sign
ax_of :: [(String, sen)]
}
data TheoryMorphism sign sen mor = TheoryMorphism {
t_source, t_target :: (Theory sign sen)
t_morphism :: mor
}
type Rule = String
type Tactic_script = String
data Proof_status sen proof_tree
= Open sen
| Disproved sen
| Proved (sen, [sen], String, proof_tree, Tactic_script)
data Prover sen proof_tree symbol = Prover {
prover_name :: String
prover_sublogic :: String
add_sym :: (symbol -> IO Bool)
remove_sym :: (symbol -> IO Bool)
add_sen :: (sen -> IO Bool)
remove_sen :: (sen -> IO Bool)
prove :: (sen -> IO [Proof_status sen proof_tree])
add_termination_info :: ([symbol] -> [(symbol, [symbol])] -> IO Bool)
remove_termination_info :: ([symbol] -> [(symbol, [symbol])] -> IO Bool)
replay :: (proof_tree -> Maybe sen)
}
data Cons_checker morphism = Cons_checker {
cons_checker_name :: String
cons_checker_sublogic :: String
cons_check :: (morphism -> IO (Bool, Tactic_script))
}
Produced by Haddock version 0.6