Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Complete Cut-Free Tableaux for Equational Simple Type Theory

Chad E. Brown, Gert Smolka

Technical Report, Saarbrücken, Germany, April 2009

We present a cut-free tableau system for a version of Church's simple type theory with primitive equality. The system is formulated with an abstract normalization operator that completely hides the details of lambda conversion. We prove completeness of the system relative to Henkin models. The proof constructs Henkin models using the novel notion of a value system.

Download PDF        Show BibTeX               

@TECHREPORT{BrownSmolkaESTT,
  title = {Complete Cut-Free Tableaux for Equational Simple Type Theory},
  author = {Chad E. Brown and Gert Smolka},
  year = {2009},
  month = {April},
  address = {{Saarbrücken, Germany}},
}

Login to edit