Incremental Proof Search in the Splitting Calculus
Christian Mahesh · 2004
This thesis presents an incremental proof search procedure based on a variable splitting sequent calculus for first-order logic without equality. By means of an index system for formulae, the calculus generates variable sharing derivations in which γ-inferences for different occurrences of the same formula introduce identical variables. Formula indices are utilized to keep track of how variables are split into different branches of a derivation. This allows closing substitutions to instantiate occurrences of the same variable differently under certain conditions. We represent closing substitutions as syntactic constraints and define an incremental method for calculating these constraints alongside derivation expansion. ii Acknowledgments During my first week as a MS student at Department of Informatics I attended a presentation concerning possible thesis topics. One of the presenters, Arild Waaler, talked for no more than three minutes about something he called “automated theorem proving”, a subject which I at that time had no prior knowledge of. Nevertheless, the way he held his short presentation immediately caught my attention. When I later asked him to be my supervisor, he accepted and invited me to attend his graduate course in logic. It was the subtle and inspiring lectures of Arild and the excellent student workshops led by teacher’s assistant Roger Antonsen which introduced me to the fascinating world of logic. Roger later became my second supervisor. The work culminating in the document you are now reading would not have been possible without the inspiration and support provided by Arild and Roger. When I have been overwhelmed by details and unable to see the big picture, Arild has many a time rescued me from “drowning”. With Roger I have had long and interesting conversations about logic and other subjects. His consuming dedication to his work is very inspiring and his scrutinizing attention to detail makes him the perfect proof reader. I sincerely hope to continue working with them both in the future! I also want to thank Martin Giese for some very helpful comments in the final stage of the writing process.