Examples
Some of these examples are not compatible with
later versions of Prover9 (note added April 2006).
Some New Features
Otter Features not (yet?) in Prover9
- Resonance Weighting
- Hot List
- Ad Hoc Term Ordering
- Ancestor Subsumption
- Dollar Evaluation
Convenience Features