Chad E. Brown ; Gert Smolka - 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 - https://doi.org/10.2168/LMCS-6(2:3)2010
Analytic Tableaux for Simple Type Theory and its First-Order FragmentArticle

Authors: Chad E. Brown ; Gert Smolka

    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.


    Volume: Volume 6, Issue 2
    Published on: June 23, 2010
    Imported on: December 18, 2009
    Keywords: Computer Science - Logic in Computer Science,03B15

    6 Documents citing this article

    Consultation statistics

    This page has been seen 994 times.
    This article's PDF has been downloaded 367 times.