Publication details

Saarland University Computer Science

Analytic Tableaux for Simple Type Theory and its First-Order Fragment

Chad E. Brown, Gert Smolka

Logical Methods in Computer Science 6(2), June 2010

We study simple type theory with primitive equality (STT) and its first-order fragment EFO, which restricts equality and quantification to base types but retains lambda abstraction and higher-order variables. As deductive system we employ a cut-free tableau calculus. We consider completeness, compactness, and existence of countable models. We prove these properties for STT with respect to Henkin models and for EFO with respect to standard models. We also show that the tableau system yields a decision procedure for three EFO fragments.

Available at LMCS

Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009