Brown, Chad E. and Smolka, Gert - Analytic Tableaux for Simple Type Theory and its First-Order Fragment

lmcs:1169 - Logical Methods in Computer Science, June 23, 2010, Volume 6, Issue 2
Analytic Tableaux for Simple Type Theory and its First-Order Fragment

Authors: Brown, Chad E. and Smolka, Gert

We study simple type theory with primitive equality (STT) and its first-order fragment EFO, which restricts equality and quantification to base types but retains lambda abstraction and higher-order variables. As deductive system we employ a cut-free tableau calculus. We consider completeness, compactness, and existence of countable models. We prove these properties for STT with respect to Henkin models and for EFO with respect to standard models. We also show that the tableau system yields a decision procedure for three EFO fragments.


Source : oai:arXiv.org:1004.1947
DOI : 10.2168/LMCS-6(2:3)2010
Volume: Volume 6, Issue 2
Published on: June 23, 2010
Submitted on: December 18, 2009
Keywords: Computer Science - Logic in Computer Science,03B15


Share

Consultation statistics

This page has been seen 48 times.
This article's PDF has been downloaded 41 times.