Research Fellow,
Precise modelling and analysis (PMA)
Office 2403, second floor,
Department of Informatics,
University of Oslo,
Norway
E-mail: chrisha (at) ifi (dot) uio (dot) no
Office phone: +47 22 85 27 45
Cell phone: +47 908 64 927
Telefax: +47 22 85 24 01 (please notify me in advance)
Snail mail address | Curriculum Vitae
List of logic resources at University of Oslo
I am currently part of the TAcS team at PMA, together with Arild Waaler and Roger Antonsen. Our goal is to investigate new techniques for proof search in tablau calculi. For the moment we are working on variable splitting, which is a way of allowing different term assignments to different branch occurrences of the same instantiation variable (free variable) in tableaux. We are developing a variable splitting sequent calculus for first-order logic and we intend to extend variable splitting to sequent calculi for other logics, e.g. modal and intuitionistic logic.
Incremental proof search is an efficient and backtracking free proof search procedure for free variable tableau calculi introduced by Martin Giese. TAcS has adopted this approach to proof search and in my Master's Thesis I have combined variable splitting and incremental proof search. We believe that incremental proof search can be transferred to calculi for other logics.
Master's Thesis: Incremental Proof Search in the Splitting Calculus color | black-and-white | bibtex
“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.
Last update: January 4th, 2007.