Publication details

Saarland University Computer Science

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               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009