My research in the area of automated deduction aims at the development
automatic proof search procedures for classical and nonclassical logics.
Together with former students from the Technical University of Darmstadt
I work on proof search methods based on matrixcharacterizations of logical
validity, a very compact representation of the search space.
We have developed a uniform proof search procedure for classical logic,
intuitionistic logic, various modal logics, fragments of linear logic, and
induction. We have also developed a uniform algorithm for transforming the
machinefound matrix proofs into sequent proofs, which enables us guide the
development of proofs in interactive assistants such as Nuprl.
