Christian Mahesh Hansen

PhD Student,
Object-orientation, modelling, and languages (OMS)

E-mail: chrisha (at) ifi (dot) uio (dot) no
Cell phone: +47 908 64 927

Research

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.

Publications

• PhD Thesis - to be published 2012
• Incremental variable splitting, Christian Mahesh Hansen, Roger Antonsen, Martin Giese, and Arild Waaler. Accepted for publication in Journal of Symbolic Computation, Special Issue on First-Order Theorem Proving, Elsevier, 2012. Published online
• Incremental Closure of Variable Splitting Tableaux, Christian Mahesh Hansen, Roger Antonsen, Arild Waaler. Position paper at Tableaux 2007, Aix en Provence, France. Download: pdf
• Incremental Proof Search in the Splitting Calculus, Christian Mahesh Hansen. Master's Thesis, Dept. of Informatics, University of Oslo, December 2004. Download: color | black-and-white | bibtex

Supervision

• Karianne Ekern: JavaSplitter. A Java Implementation of Variable Splitting Proof Search    PDF
Short Master's Thesis supervised spring 2005 in cooperation with Arild Waaler.

Private

“The world needs open hearts and open minds, and it is not through rigid systems, whether old or new, that these can be derived.”
—Bertrand Russell

“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.