C | |
| clause [Prover] | |
| clause [Reasoner] | |
| clause [Encoding] | |
| consequence [Reasoner] | |
F | |
| fact [Reasoner] | |
| foclause [Plugin] | |
| foclause [Encoding] | |
| foterm [Encoding] | |
H | |
| hoclause [Encoding] | |
| hoterm [Encoding] | |
L | |
| lit [Encoding] | |
O | |
| or_error [Prover] | |
P | |
| printer [Encoding] | |
| proof [Reasoner] | |
| property [Reasoner] | |
T | |
| t [Prover] |
Meta-prover
|
| t [Plugin.Set] | |
| t [Reasoner.Proof] | |
| t [Reasoner.Clause] | |
| t [Reasoner] |
A DB that holds a saturated set of Horn clauses and facts
|
| t [Encoding.EncodedClause] | |
| term [Plugin] | |
| term [Reasoner] | |
| ty [Plugin] | |
| ty [Reasoner] | |
W | |
| with_proof [Reasoner.Proof] |