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
Wed Sep 16 10:47:00 2009