Interface | Description |
---|---|
LemmaGenerator |
A Lemma Generator translates a taclet to its corresponding
first order logic formula thats validity implies the validity
of the taclet.
|
TacletSoundnessPOLoader.LoaderListener | |
TacletSoundnessPOLoader.TacletFilter |
Class | Description |
---|---|
AutomaticProver |
A very simple type of prover, but it is sufficient for the automatic lemmata
handling: Normally there is a mechanism for choosing the next goal in a
cyclic way if for the currently chosen goal no rules are left that could be
applied.
|
DefaultLemmaGenerator |
The default lemma generator: Supports only certain types of
taclets.
|
EmptyEnvInput | |
GenericRemovingLemmaGenerator |
Generic removing lemma generator adds the default implementation only that all
GenericSort s are replaced to equally named ProxySort s. |
LemmaFormula | |
ProofObligationCreator |
Creates for a given set of taclets the corresponding set of proof
obligation.
|
TacletLoader | |
TacletLoader.KeYsTacletsLoader | |
TacletLoader.TacletFromFileLoader | |
TacletProofObligationInput |
The Class TacletProofObligationInput is a special purpose proof obligations
for taclet proofs.
|
TacletSoundnessPOLoader | |
TacletSoundnessPOLoader.TacletInfo | |
UserDefinedSymbols | |
UserDefinedSymbols.NamedComparator |