| 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
GenericSorts are replaced to equally named ProxySorts. |
| 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 |