PTTP+GLiDeS
Abstract
PTTP+GLiDeS is a semantically guided linear deduction theorem prover, built
from PTTP and MACE.
PTTP+GLiDeS implements linear deduction using the Model
Elimination paradigm.
PTTP+GLiDeS takes problems in clause normal form, uses MACE to generate
semantic information about the clauses, and then uses the semantic
information to guide the PTTP search for a proof.