Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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)       

@INPROCEEDINGS{BrownSmolkaBasic,
  title = {Terminating Tableaux for the Basic Fragment of Simple Type Theory},
  author = {Chad E. Brown and Gert Smolka},
  year = {2009},
  month = {Jul},
  editor = {M. Giese and A. Waaler},
  publisher = {Springer},
  booktitle = {TABLEAUX 2009},
  series = {{LNCS (LNAI)}},
  volume = {5607},
  pages = {{138-151}},
}

Login to edit