Bachelor's Thesis: Towards a Semiautomatic Higher Order Tableau Prover

Author: Matthias Höschele
Advisor: Dr. Chad E Brown
Advisor: Professor Dr. Gert Smolka

Current State

• Full port to GWT. Current development snapshot available.
• Working on JitPro. Current development snapshot available.
• Experimenting with Coq in order to compare the ways of proving simple higher-order claims to the proves done in JitPro.
• Implementing a decision procedure in Google Web Toolkit.
• I have given my first talk "Comparing JitPro and Coq", have a look at the slides.

Description

JITPRO is a JavaScript Interactive Higher-Order Tableau Prover that was developed by Chad E Brown. At the moment JitPro asks the user to enter the problem and then displays a tableau branch, where you can easily apply a rule by clicking on the corresponding button. JitPro turned out to be a very useful tool for all students of the Introduction to Computational Logic SS08 course, because it offers a quick way to experiment with tableau proofs that would have took much longer by only using pen and paper.

However, there is much more that could be done to help users in doing tableau proofs for example simplifying a branch by applying "safe" rules automatically. Features that can be used to automatize proving to a certain degree give a user the opportunity to focus on crucial points of their proofs like instantiations of Forall and therefore allow users to forget about certain details and prove on a comparatively high level.

Goal

The goal of this project is to make proving with JitPro easier. In order to do so JitPro will be provided with several automatized proof assistance methods. It will also be extended with a structured view that will prevent users form getting lost in big proofs and present the rules available to apply in a ordered manner.