Christoph Wernhard – Computer Science

Research Interests
Logic-Based Knowledge Representation. In particular, expressing knowledge processing operations in semantically founded and integrable ways by variants of second-order quantifier elimination. Automated Theorem Proving in First-Order Logic, along with generalizations such as Craig interpolation and second-order quantifier elimination. Practical applications of knowledge-based techniques.
Software Systems
  • The CD Tools library for experimenting with condensed detachment in first-order ATP
  • The PIE environment for first-order-based Proving, Interpolating and Eliminating
  • The KBSET environment: Knowledge-Based Support for Scholarly Editing and Text processing
Research Projects
Links to the Past
Teaching (at TU Dresden) | The European PhD Program in Computational Logic (EPCL) | Deduktionstreffen 2005 in Koblenz | KRHyper Model Generation and Theorem Proving System | DFG Project MoDeDok: Model Based Deduction (2003-06 at Koblenz University) | BMBF Project In2Math (2001-03 at Koblenz University) | Persist AG – Database and Semantic Web Technology (1999-2001, Teltow) | DFG Project ILF: Integrating Logical Functions (1996-98 at Humboldt-Universit├Ąt, Berlin) | before...