Julian Backes

Saarland University Computer Science

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


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.