Publication details

Saarland University Computer Science

Terminating Tableaux for the Basic Fragment of Simple Type Theory

Chad E. Brown, Gert Smolka

TABLEAUX 2009, Vol. 5607 of LNCS (LNAI), pp. 138-151, Springer, July 2009

We consider the basic fragment of simple type theory, which restricts equations to base types and disallows lambda abstractions and quantifiers. We show that this fragment has the finite model property and that satisfiability can be decided with a terminating tableau system. Both results are with respect to standard models.

Download PDF        Show BibTeX        Download slides (PDF)       

Login to edit

Legal notice, Privacy policy