Terminating Tableaux for the Basic Fragment of Simple Type Theory

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.

• Type: Conference
• Year: 2009
• Where: TABLEAUX
• Authors: Chad E. Brown, Gert Smolka
• Keywords: Artificial Intelligence, Lambda Abstractions, TABLEAUX 2009, Terminating Tableau System, finite Model Property