PTTP+GLiDeS: Guiding linear deductions with semantics

Abstract

Using semantics to guide automated theorem proving systems is an under-utilised technique. In linear deduction, semantic guidance has received only limited attention. This research is developing semantic guidance for linear deduction in the Model Elimination paradigm. Search pruning, at the possible loss of some refutation completeness, and search guidance, are being considered. This paper describes PTTP+GLiDeS, a PTTP style prover augmented with a semantic pruning mechanism, GLiDeS. PTTP+GLiDeS combines a modified version of Stickel’s PTTP prover with the model generator MACE.