Object-orientation, modelling, and languages (OMS)
Department of Informatics,
University of Oslo, Norway
E-mail: chrisha (at) ifi (dot) uio (dot) no
Cell phone: +47 908 64 927
Snail mail address
Curriculum Vitae: please contact me for a copy
I am currently nearing the end of my PhD project, supervised by Martin Giese and Arild Waaler. The subject of study is the use of variable splitting in theorem provers for first-order logic, and the main goal is to combine the work on variable splitting proposed by Antonsen and Waaler with the incremental closure proof procedure introduced by Giese.
In free-variable tableau calculi, free variables are introduced as place-holders when expanding universal formulas in order to postpone the choice of an instantiation. Free variables are instantiated when branches are closed, by unifying potentially complementary formulas on a branch. The expansion of disjunctive formulas splits a proof into several branches, and the same free variable can occur on more than one branch. Usually, occurrences of a free variable on different branches have to be instantiated consistently to ensure soundness.
Antonsen and Waaler have analyzed the dependency between branching and the instantiation of free variables and have arrived at a criterion that, in some cases, permits to instantiate a free variable differently on different branches. Such divergent instantiation is referred to as variable splitting.
Incremental proof search is an efficient and backtracking free proof search procedure for free variable tableau calculi introduced by Giese. The idea is to keep track of the set of closing substitutions for every subderivation during proof search, and updating this information whenever a new complimentary pair of literals is found. Syntactic unification constraints are used to represent sets of substitutions. Incremental closure avoids the repeated construction and closure of sub-derivations necessary in the more usual iterative deepening procedure.
We have arrived at a prototype implementation of a theorem prover with variable splitting. You can read more about it here.
The world needs open hearts and open minds, and
it is not through rigid systems, whether old or new, that these can be
To see what isn't true is easy. But to see what
is true will take some doing.
Janwillem van de Wetering
Although I do my best not to be someone, my self looks something like this.
This page was last modified on Sunday, 29-Apr-2012 19:24:23 CEST.