Introduction
- Semantically Guided Systems
- The Geometry-Theorem Proving Machine
(natural)
- CLIN-S (hyperlinking)
- SCOTT (hyperresolution)
- RAMCS (constrained clauses)
- GLiDeS - Guiding Linear
Deductions with Semantics
- Pruning
- Search reordering
- PTTP+GLiDeS - Applies GLiDeS to PTTP