Publication details

Saarland University Computer Science

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               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009