Publication details

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

@ARTICLE{BrownSmolka2010,
  title = {Analytic Tableaux for Simple Type Theory and its First-Order Fragment},
  author = {Chad E. Brown and Gert Smolka},
  year = {2010},
  month = {Jun},
  journal = {Logical Methods in Computer Science},
  volume = {6},
  number = {2},
  address = {{Saarbr{\"u}cken, Germany}},
  note = {http://www.lmcs-online.org/ojs/viewarticle.php?id=641&layout=abstract},
}

Webmaster, Wed Sep 16 10:47:00 2009