About me
Dr. Christoph Sticksel
Postdoctoral Research Fellow (EPSRC PhD Plus pilot scheme, now Doctoral Prize) at The University of Manchester (until September 2011)
School of Computer Science, Formal Methods Group
Project title: “Instantiation-Based Reasoning – Equality and Theories beyond”
Lay summary of my
research
(read this if you want the jargon-free answer
to what I am doing and what it is good for)
Contact
Email: csticksel@cs.man.ac.uk
Room 2.108, Kilburn Building, campus map no. 39
Office phone: +44 (0) 161 275 6266 (Internal: 56266)
Research
(Also check my lay abstract if you don't want the jargon below)
I am interested in automated reasoning with instantiation-based methods and there in particular in handling theories like equality and beyond in a robust way.
My research is focussed on the Inst-Gen method by Ganzinger and Korovin which combines ground reasoning by a modular off-the-shelf solver with efficient first-order reasoning. Clause instances are generated until either the ground solver can witness unsatisfiability or the existence of a first-order model has been shown.
I am extending the iProver system as iProver-Eq integrating an SMT solver for ground reasoning and a labelled superposition-based calculus for first-order reasoning modulo equality.
We have entered iProver-Eq into three CADE ATP system competitions (CASC-22, CASC-J5 and CASC-23) and are constantly evolving it, without having a formal release. Drop me a line if you have interesting problems you want to try.
Publications
Christoph Sticksel, “Z3 for iProver-Eq: Efficient Ground Solving for Instantiation-based First-order Reasoning”. Talk given at Z3 Special Interest Group meeting, Cambridge, UK, November 2011. (Slides)
Christoph Sticksel, “Efficient Equational Reasoning in the Inst-Gen Framework”. Ph.D. thesis, The University of Manchester, 2011. (PDF)
Christoph Sticksel, “Instantiation-based Methods for Equational Reasoning and Theories Beyond”. Talk given at Max-Planck-Institut für Informatik, Saarbrücken, January 2011. (Slides)
Konstantin Korovin and Christoph Sticksel, “Labelled Unit Superposition Calculi for Instantiation-based Reasoning” in 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-17, ser. Lecture Notes in Computer Science, vol. 6397. Berlin / Heidelberg: Springer, 2010, pp. 459-473. (PDF | Slides | BibTeX ) The original publication is available at www.springerlink.com
Konstantin Korovin and Christoph Sticksel, “iProver-Eq: An Instantiation-based Theorem Prover with Equality” in 5th International Joint Conference on Automated Reasoning, IJCAR 2010, ser. Lecture Notes in Computer Science, vol. 6173. Berlin / Heidelberg: Springer, 2010, pp. 196-202. (PDF | Slides | BibTeX) The original publication is available at www.springerlink.com
Konstantin Korovin and Christoph Sticksel, “iProver-Eq: An Instantiation-based Theorem Prover with Equality”, in 17th Workshop on Automated Reasoning, ARW 2010, University of Westminster, March 2010, pp. 22-23. (PDF)
Christoph Sticksel, “Efficient Ground Satisfiability Solving in an Instantiation-based Method for First-order Theorem Proving” in 16th Workshop on Automated Reasoning, ARW 2009, University of Liverpool, April 2009, pp. 39-40. (PDF)
Christoph Sticksel, “Automated Theorem Proving in Interactive Proof Construction”, Diplomarbeit (Master's dissertation), Fakultät für Informatik, Universität Karlsruhe, 2007 (PDF)
Biography
PhD in Computer Science from The University of Manchester, UK under supervision Konstantin Korovin and Renate Schmidt, thesis “Efficient Equational Reasoning in the Inst-Gen Framework”. Ph.D. thesis, The University of Manchester, 2011. (PDF)
“Diplom” in Computer Science from the University of Karlsruhe, Germany (4.5 year course equivalent to a Master's degree)
Diplom dissertation “Automated Theorem Proving in Interactive Proof Construction” at the Australian National University, Canberra / NICTA under supervision of Peter Baumgartner (NICTA) and P. H. Schmitt (Uni Karlsruhe) (PDF)
Links
My private blog (proof of my laziness)
