hets -- a heterogenous Specification (CASL) tool set
Contents
Index
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