Sciweavers

TPHOL
2009
IEEE

Extended First-Order Logic

13 years 10 months ago
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.
Chad E. Brown, Gert Smolka
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where TPHOL
Authors Chad E. Brown, Gert Smolka
Comments (0)