Master's Thesis: Tableaux for Higher-Order Logic with If-Then-Else, Description and Choice

Author: Julian Backes
Advisor: Dr. Chad E. Brown
Supervisor: Professor Dr. Gert Smolka

Current State

• Download the thesis
• Third talk: Friday, April 9, 2010, 14:15. Building E1.3, Room 528 (download slides)
• Second talk: Friday, August 28, 2009, 14:15. Building E1.3, Room 528 (download slides)
• First talk: Friday, June 26, 2009, 14:15. Building E1.3, Room 528 (download slides)

Description

In the past few months, Brown and Smolka published three papers about specific fragments of higher order logic and presented corresponding tableau systems which are complete, cut-free and in one case terminating. I am planning to extend these tableau systems to include rules for an if-then-else operator, a description operator and a choice operator while preserving the existing properties of the systems. I will give rules for an if-then-else operator and propose rules for a choice operator. The rules for a choice operator are based on a paper by Mints from 1996.

References

• Chad E. Brown, G. Smolka: Terminating Tableaux for the Basic Fragment of Simple Type Theory. TABLEAUX 2009:138-151, Springer LNCS 5607.
• Chad E. Brown, G. Smolka: Extended First-Order Logic. TPHOLs 2009, Springer LNCS 5674.
• Chad E. Brown, G. Smolka: Complete Cut-Free Tableaux for Equational Simple Type Theory. 2009.
• G. Mints: Cut-Elimination for Simple Type Theory with an Axiom of Choice. The Journal of Symbolic Logic, Vol. 64, No. 2., pp. 479-485. 1999.
• G. Takeuti: Proof Theory (Studies in Logic and the Foundations of Mathematics). Elsevier Science Ltd, 2 Rev Sub edition. 1987.