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.

Papers

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

• Proof Structures: Proofs as Formal Objects and as Data Structures
• The Second-Order Approach and its Application to View-Based Query Processing

Advertisement

• Book project: Theory and Applications of Craig Interpolation
  Edited by Balder ten Cate, Jean Christoph Jung, Patrick Koopmann, Christoph Wernhard and Frank Wolter. To appear in 2025/2026, open access.

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

---

E-mail: info@christophwernhard.com