Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Extended First-Order Logic

Chad E. Brown, Gert Smolka

Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Proceedings, Vol. 5674 of LNCS, pp. 164--179, Springer, August 2009

We consider the EFO fragment of simple type theory, which restricts quantification and equality to base types but retains lambda abstractions and higher-order variables. We show that this fragment enjoys the characteristic properties of first-order logic: complete proof systems, compactness, and countable models. We obtain these results with an analytic tableau system and a concomitant model existence lemma. All results are with respect to standard models. The tableau system is well-suited for proof search and yields decision procedures for substantial fragments of EFO.

Download PDF        Show BibTeX               

@INPROCEEDINGS{BrownSmolkaEFO,
  title = {Extended First-Order Logic},
  author = {Chad E. Brown and Gert Smolka},
  year = {2009},
  month = {Aug},
  editor = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
  publisher = {Springer},
  booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Proceedings},
  series = {{LNCS}},
  volume = {5674},
  pages = {164--179},
}

Login to edit