GLiDeS' Models

Abstract

PTTP+GLiDeS is a linear deduction theorem prover that uses semantics to guided its search for a proof. The semantics are automatically generated by using MACE to find a model for a subset of the input clause set. Results have shown that where an ``effective'' model is found, the guidance it provides is of great benefit. This paper discusses how MACE is used in PTTP+GLiDeS, and what properties are desirable in models and model generators for this application.