Extended First-Order Logic

ion 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.

• Type: Conference
• Year: 2009
• Where: TPHOL
• Authors: Chad E. Brown, Gert Smolka
• Keywords: Artificial Intelligence, Complete Proof Systems, Concomitant Model Existence, TPHOL 2009, Yields Decision Procedures