Papers

Publications
Unpublished Material

Publications

Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic

Jan Heuer and Christoph Wernhard

In Chris Benzmüller, Marjin Heule, and Renate Schmidt, editors, International Joint Conference on Automated Reasoning, IJCAR 2024, LNCS (LNAI). Springer, 2024.

To appear, preprint: https://arxiv.org/abs/2402.07696.

[ bib | Abstract ]

Synthesizing Nested Relational Queries from Implicit Specifications: Via Model Theory and via Proof Theory

Michael Benedikt, Cécilia Pradic, and Christoph Wernhard

Logical Methods in Computer Science, 2024.

To appear, preprint: http://arxiv.org/abs/2212.03085.

[ bib | Abstract ]

Structure-Generating First-Order Theorem Proving

Christoph Wernhard

In Jens Otten and Wolfgang Bibel, editors, AReCCa 2023 - Automated Reasoning with Connection Calculi, International Workshop, volume 3613 of CEUR Workshop Proceedings, pages 64-83. CEUR-WS.org, 2024.

[ Presentation slides ].

[ bib | .pdf | Abstract ]

Range-Restricted and Horn Interpolation through Clausal Tableaux

Christoph Wernhard

In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, volume 14278 of LNCS (LNAI), pages 3-23. Springer, 2023.

[ Preprint (extended version): https://arxiv.org/abs/2306.03572 | Presentation slides ].

[ bib | DOI | Abstract ]

Lemmas: Generation, Selection, Application

Michael Rawson, Christoph Wernhard, Zsolt Zombori, and Wolfgang Bibel

[ Preprint (extended version): https://arxiv.org/abs/2303.05854 | Presentation slides ].

[ bib | DOI | Abstract ]

Learning to Identify Useful Lemmas from Failure

Michael Rawson, Christoph Wernhard, and Zsolt Zombori

In Michael R. Douglas, Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, and Josef Urban, editors, 8th Conference on Artificial Intelligence and Theorem Proving, AITP 2023 (Informal Book of Abstracts), 2023.

[ Extended abstract | Presentation slides ].

[ bib ]

Investigations into Proof Structures

Christoph Wernhard and Wolfgang Bibel

2023.

[ Preprint (submitted): https://arxiv.org/abs/2304.12827 ].

[ bib | Abstract ]

Synthesizing Nested Relational Queries from Implicit Specifications

Michael Benedikt, Cécilia Pradic, and Christoph Wernhard

In Principles of Database Systems, PODS 23, pages 33-45, 2023.

[ bib | DOI | Abstract ]

Compressed Combinatory Proof Structures and Blending Goal- with Axiom-Driven Reasoning: Perspectives for First-Order ATP with Condensed Detachment and Clausal Tableaux

Christoph Wernhard

In Michael R. Douglas, Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, and Josef Urban, editors, 7th Conference on Artificial Intelligence and Theorem Proving, AITP 2022 (Informal Book of Abstracts), 2022.

[ Extended abstract | Presentation slides ].

[ bib ]

Generating Compressed Combinatory Proof Structures - An Approach to Automated First-Order Theorem Proving

Christoph Wernhard

In Boris Konev, Claudia Schon, and Alexander Steen, editors, 8th Workshop on Practical Aspects of Automated Reasoning, PAAR 2022, volume 3201 of CEUR Workshop Proceedings. CEUR-WS.org, 2022.

[ Preprint: https://arxiv.org/abs/2209.12592 ].

[ bib | Abstract ]

CD Tools - Condensed Detachment and Structure Generating Theorem Proving (System Description)

Christoph Wernhard

Technical report, 2022.

https://arxiv.org/abs/2207.08453.

[ bib | DOI | Abstract ]

Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021)

Renate A. Schmidt, Christoph Wernhard, and Yizheng Zhao, editors

Volume 3009 of CEUR Workshop Proceedings, Aachen, 2021. CEUR-WS.org.

[ bib | http ]

Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof

Christoph Wernhard

In Renate A. Schmidt, Christoph Wernhard, and Yizheng Zhao, editors, Proceedings of the Second Workshop on Second-Order Elimination and Related Topics (SOQE 2021), volume 3009 of CEUR Workshop Proceedings, pages 98-111, 2021.

[ Preprint (extended version): https://arxiv.org/abs/2110.11108 ].

[ bib | .pdf | Abstract ]

Learning from Łukasiewicz and Meredith: Investigations into Proof Structures

Christoph Wernhard and Wolfgang Bibel

In André Platzer and Geoff Sutcliffe, editors, Automated Deduction: CADE 2021, volume 12699 of LNCS (LNAI), pages 58-75. Springer, 2021.

[ Preprint (extended version): https://arxiv.org/abs/2104.13645 | Presentation slides ].

[ bib | DOI | Abstract ]

Craig Interpolation with Clausal First-Order Tableaux

Christoph Wernhard

Journal of Automated Reasoning, 65(5):647-690, 2021.

[ Preprint: https://arxiv.org/abs/2008.03489 ].

[ bib | DOI | Abstract ]

Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic

Christoph Wernhard

In Petra Hofstedt, Salvador Abreu, Ulrich John, Herbert Kuchen, and Dietmar Seipel, editors, Declarative Programming and Knowledge Management (DECLARE 2019), Revised Selected Papers, volume 12057 of LNCS (LNAI), pages 160-177. Springer, 2020.

[ Preprint: https://arxiv.org/abs/2002.10892 ].

[ bib | DOI | Abstract ]

KBSET - Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative LaTeX Markup and a Core Written in SWI-Prolog

Jana Kittelmann and Christoph Wernhard

[ Preprint: https://arxiv.org/abs/2002.10329 ].

[ bib | DOI | Abstract ]

Von der Transkription zur Wissensbasis. Zum Zusammenspiel von digitalen Editionstechniken und Formen der Wissensrepräsentation am Beispiel von Korrespondenzen Johann Georg Sulzers

Jana Kittelmann and Christoph Wernhard

In Jana Kittelmann and Anne Purschwitz, editors, Aufklärungsforschung digital. Konzepte, Methoden, Perspektiven, volume 10/2019 of IZEA - Kleine Schriften, pages 84-114. Mitteldeutscher Verlag, 2019.

[ Preprint: http://www.sulzer-digital.de/papiere/transkription_wissensbasis.pdf ].

[ bib ]

PIE - Proving, Interpolating and Eliminating on the Basis of First-Order Logic

Christoph Wernhard

In Salvador Abreu, Petra Hofstedt, Ulrich John, Herbert Kuchen, and Dietmar Seipel, editors, Pre-proceedings of the DECLARE 2019 Conference, volume abs/1909.04870 of CoRR, 2019.

[ bib | arXiv | Abstract ]

KBSET - Knowledge-Based Support for Scholarly Editing and Text Processing

Jana Kittelmann and Christoph Wernhard

In Salvador Abreu, Petra Hofstedt, Ulrich John, Herbert Kuchen, and Dietmar Seipel, editors, Pre-proceedings of the DECLARE 2019 Conference, volume abs/1909.04870 of CoRR, 2019.

[ bib | arXiv | Abstract ]

Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux

Christoph Wernhard

Technical Report Knowledge Representation and Reasoning 18-01, Technische Universität Dresden, 2018.

[ bib | arXiv | Abstract ]

Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics, SOQE 2017

Patrick Koopmann, Sebastian Rudolph, Renate A. Schmidt, and Christoph Wernhard, editors

Volume 2013 of CEUR Workshop Proceedings. CEUR-WS.org, 2017.

[ bib | http ]

Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas

Christoph Wernhard

In Patrick Koopmann, Sebastian Rudolph, Renate A. Schmidt, and Christoph Wernhard, editors, Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics, SOQE 2017, volume 2013 of CEUR Workshop Proceedings, pages 82-98. CEUR-WS.org, 2017.

[ bib | .pdf | Abstract ]

The Boolean Solution Problem from the Perspective of Predicate Logic - Extended Version

Christoph Wernhard

Technical Report Knowledge Representation and Reasoning 17-01, Technische Universität Dresden, 2017.

[ bib | arXiv | Abstract ]

The Boolean Solution Problem from the Perspective of Predicate Logic

Christoph Wernhard

In Clare Dixon and Marcelo Finger, editors, 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017, volume 10483 of LNCS (LNAI), pages 333-350. Springer, 2017.

[ Preprint | Presentation slides ].

[ bib | DOI | Abstract ]

Craig Interpolation and Query Reformulation with Clausal First-Order Tableaux

Christoph Wernhard

Poster presentation at Automated Reasoning with Analytic Tableaux and Related Methods: 26th International Conference, TABLEAUX 2017, 2017.

[ bib | .pdf ]

The PIE system for Proving, Interpolating and Eliminating

Christoph Wernhard

In Pascal Fontaine, Stephan Schulz, and Josef Urban, editors, 5th Workshop on Practical Aspects of Automated Reasoning, PAAR 2016, volume 1635 of CEUR Workshop Proceedings, pages 125-138. CEUR-WS.org, 2016.

[ bib | .pdf | Abstract ]

Towards Knowledge-Based Assistance for Scholarly Editing

Jana Kittelmann and Christoph Wernhard

In Thomas C. Hales, Cezary Kaliszyk, Stephan Schulz, and Josef Urban, editors, 1st Conference on Artificial Intelligence and Theorem Proving, AITP 2016 (Book of Abstracts), pages 29-31, 2016.

[ Presentation slides ].

[ bib | http | Abstract ]

Knowledge-Based Support for Scholarly Editing and Text Processing

Jana Kittelmann and Christoph Wernhard

In DHd 2016 - Digital Humanities im deutschsprachigen Raum: Modellierung - Vernetzung - Visualisierung. Die Digital Humanities als fächerübergreifendes Forschungsparadigma. Konferenzabstracts, pages 178-181, Duisburg, 2016. nisaba verlag.

[ Presentation slides (in German) ].

[ bib | DOI ]

Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic

Christoph Wernhard

Technical Report Knowledge Representation and Reasoning 15-05, Technische Universität Dresden, 2015.

Revised 2017.

[ bib | arXiv | Abstract ]

Some Fragments Towards Establishing Completeness Properties of Second-Order Quantifier Elimination Methods

Christoph Wernhard

Poster presentation at Jahrestreffen der GI Fachgruppe Deduktionssysteme, associated with CADE-25, 2015.

[ bib | .pdf ]

Second-Order Quantifier Elimination on Relational Monadic Formulas - A Basic Method and Some Less Expected Applications

Christoph Wernhard

In Hans de Nivelle, editor, Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015, volume 9323 of LNCS (LNAI), pages 249-265. Springer, 2015.

[ Presentation slides ].

[ bib | DOI | Abstract ]

Second-Order Quantifier Elimination on Relational Monadic Formulas - A Basic Method and Some Less Expected Applications (Extended Version)

Christoph Wernhard

Technical Report Knowledge Representation and Reasoning 15-04, Technische Universität Dresden, 2015.

[ bib | .pdf | Abstract ]

Second-Order Characterizations of Definientia in Formula Classes

Christoph Wernhard

In Alexander Bolotov and Manfred Kerber, editors, Joint Automated Reasoning Workshop and Deduktionstreffen, ARW-DT 2014, pages 36-37, 2014.

Workshop presentation [ Slides ].

[ bib | .pdf ]

Application Patterns of Projection/Forgetting

Christoph Wernhard

In Laura Kovacs and Georg Weissenbacher, editors, Workshop on Interpolation: From Proofs to Applications, iPRA 2014, 2014.

Workshop presentation [ Slides ].

[ bib | .pdf ]

Second-Order Characterizations of Definientia in Formula Classes

Christoph Wernhard

Technical Report Knowledge Representation and Reasoning 14-03, Technische Universität Dresden, 2014.

[ bib | .pdf | Abstract ]

Semantik, Linked Data, Web-Präsentation: Grundlagen der Nachlasserschließung im Portal www.pueckler-digital.de

Jana Kittelmann and Christoph Wernhard

In Anne Baillot and Anna Busch, editors, Workshop Datenmodellierung in digitalen Briefeditionen und ihre interpretatorische Leistung. Humboldt-Universität zu Berlin, 2014.

Poster presentation, [ Abstract | Poster ].

[ bib ]

Expressing View-Based Query Processing and Related Approaches with Second-Order Operators

Christoph Wernhard

Technical Report Knowledge Representation and Reasoning 14-02, Technische Universität Dresden, 2014.

[ bib | .pdf ]

Modeling the Suppression Task under Weak Completion and Well-Founded Semantics

Emmanuelle-Anna Dietz, Steffen Hölldobler, and Christoph Wernhard

Journal of Applied Non-Classsical Logics, 24(1-2):61-85, 2014.

[ bib ]

Computing with Logic as Operator Elimination: The ToyElim System

Christoph Wernhard

In Hans Tompits, Salvador Abreu, Johannes Oetsch, Jörg Pührer, Dietmar Seipel, Masanobu Umeda, and Armin Wolf, editors, Applications of Declarative Programming and Knowledge Management, 19th International Conference (INAP 2011) and 25th Workshop on Logic Programming (WLP 2011), Revised Selected Papers, volume 7773 of LNCS (LNAI), pages 289-296. Springer, 2013.

[ Preprint ].

[ bib | DOI | Abstract ]

Semantik, Web, Metadaten und digitale Edition: Grundlagen und Ziele der Erschließung neuer Quellen des Branitzer Pückler-Archivs

Jana Kittelmann and Christoph Wernhard

In Irene Krebs et al., editors, Resonanzen. Pücklerforschung im Spannungsfeld zwischen Wissenschaft und Kunst. Ein Konferenzbericht., pages 179-202. trafo Verlag, Berlin, 2013.

[ bib ]

Möglichkeiten der Repräsentation von Nachlassarchiven im Web

Jana Kittelmann and Christoph Wernhard

In Fachtagung Semantische Technologien - Verwertungsstrategien und Konvergenz, Humboldt-Universität zu Berlin, Position Papers, 2013.

[ bib | http ]

Abduction in Logic Programming as Second-Order Quantifier Elimination

Christoph Wernhard

In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, 9th International Symposium on Frontiers of Combining Systems, FroCoS 2013, volume 8152 of LNCS (LNAI), pages 103-119. Springer, 2013.

[ Preprint (extended version) ].

[ bib | DOI | Abstract ]

Soundness of Inprocessing in Clause Sharing SAT Solvers

Norbert Manthey, Tobias Philipp, and Christoph Wernhard

In Matti Järvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing, 16th International Conference, SAT 2013, volume 7962 of LNCS, pages 22-39. Springer, 2013.

Received the SAT 2013 Best Paper Award [ Preprint ].

[ bib | DOI | Abstract ]

Towards a Declarative Approach to Model Human Reasoning with Nonmonotonic Logics

Christoph Wernhard

In Thomas Barkowsky, Marco Ragni, and Frieder Stolzenburg, editors, Human Reasoning and Automated Deduction: KI 2012 Workshop Proceedings, volume SFB/TR 8 Report 032-09/2012 of Report Series of the Transregional Collaborative Research Center SFB/TR 8 Spatial Cognition, pages 41-48. Universität Bremen / Universität Freiburg, Germany, 2012.

(http://cs.christophwernhard.com/papers/hrad2012.pdf).

[ bib | Abstract ]

Projection and Scope-Determined Circumscription

Christoph Wernhard

Journal of Symbolic Computation, 47:1089-1108, 2012.

[ Preprint ].

[ bib | DOI | Abstract ]

Forward Human Reasoning Modeled by Logic Programming Modeled by Classical Logic with Circumscription and Projection

Christoph Wernhard

Technical Report Knowledge Representation and Reasoning 11-07, Technische Universität Dresden, 2011.

[ bib | .pdf | Abstract ]

Computing with Logic as Operator Elimination: The ToyElim System

Christoph Wernhard

In Proceedings of the 25th Workshop on Logic Programming, WLP 2011, Infsys Research Report 1843-11-06, pages 94-98. Technische Universität Wien, 2011.

[ bib | arXiv | Abstract ]

An Abductive Model for Human Reasoning

Steffen Hölldobler, Tobias Philipp, and Christoph Wernhard

In Logical Formalizations of Commonsense Reasoning, Papers from the AAAI 2011 Spring Symposium, AAAI Spring Symposium Series Technical Reports, pages 135-138. AAAI Press, 2011.

[ Preprint (extended version): http://www.wv.inf.tu-dresden.de/Publications/2010/HoelldoblerPhilippWernhard.pdf ].

[ bib | Abstract ]

Circumscription and Projection as Primitives of Logic Programming

Christoph Wernhard

In M. Hermenegildo and T. Schaub, editors, Technical Communications of the 26th International Conference on Logic Programming, ICLP'10, volume 7 of Leibniz International Proceedings in Informatics (LIPIcs), pages 202-211, Dagstuhl, Germany, 2010. Schloss Dagstuhl-Leibniz-Zentrum für Informatik.

[ Preprint (extended version) ].

[ bib | DOI | http | Abstract ]

Literal Projection and Circumscription

Christoph Wernhard

In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Proceedings of the 7th International Workshop on First-Order Theorem Proving, FTP'09, volume 556 of CEUR Workshop Proceedings, pages 60-74. CEUR-WS.org, 2010.

[ Preprint (extended version) ].

[ bib | http | Abstract ]

Tableaux for Projection Computation and Knowledge Compilation

Christoph Wernhard

In Martin Giese and Arild Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods: 18th International Conference, TABLEAUX 2009, volume 5607 of LNCS (LNAI), pages 325-340. Springer, 2009.

[ bib | DOI | .pdf | Abstract ]

Automated Deduction for Projection Elimination

Christoph Wernhard

Number 324 in Dissertations in Artificial Intelligence. AKA Verlag/IOS Press, Heidelberg, Amsterdam, 2009.

[ bib | http | Abstract ]

HydraSAT 2009.3 Solver Description

Christoph Baldow, Friedrich Gräter, Steffen Hölldobler, Norbert Manthey, Max Seelemann, Peter Steinke, Christoph Wernhard, Konrad Winkler, and Erik Zenker

In Daniel Le Berre et al., editor, SAT 2009 Competitive Event Booklet, pages 15-16, 2009.

[ bib | .pdf ]

Literal Projection for First-Order Logic

Christoph Wernhard

In Steffen Hölldobler, Carsten Lutz, and Heinrich Wansing, editors, Logics in Artificial Intelligence: 11th European Conference, JELIA 08, volume 5293 of LNCS (LNAI), pages 389-402. Springer, 2008.

[ Preprint (extended version) ].

[ bib | DOI | Abstract ]

System Description: E-KRHyper

Björn Pelzer and Christoph Wernhard

In Frank Pfenning, editor, Automated Deduction: CADE-21, volume 4603 of LNCS (LNAI), pages 503-513. Springer, 2007.

[ bib | DOI | .pdf | Abstract ]

Tableaux Between Proving, Projection and Compilation

Christoph Wernhard

Technical Report Arbeitsberichte aus dem Fachbereich Informatik 18/2007, Universität Koblenz-Landau, Institut für Informatik, Universitätsstr. 1, 56070 Koblenz, Germany, 2007.

[ bib | Abstract ]

Semantic Knowledge Partitioning

Christoph Wernhard

In José Júlio Alferes and João Leite Leite, editors, Logics in Artificial Intelligence: 9th European Conference, JELIA 04, volume 3229 of LNCS (LNAI), pages 552-564. Springer, 2004.

[ bib | DOI | .ps | Abstract ]

Semantic Knowledge Partitioning (Extended Abstract)

Christoph Wernhard

In Ulrike Sattler, editor, Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning, IJCAR 2004, volume 106 of CEUR Workshop Proceedings. CEUR-WS.org, 2004.

[ bib | http ]

KRHyper Inside - Model Based Deduction in Applications

Peter Baumgartner, Ulrich Furbach, Margret Gross-Hardt, Thomas Kleemann, and Christoph Wernhard

In Proceedings of the CADE-19 workshop Challenges and Novel Applications for Automated Reasoning, pages 55-72, 2003.

[ bib | .ps | Abstract ]

System Description: KRHyper

Christoph Wernhard

Technical Report Fachberichte Informatik 14-2003, Universität Koblenz-Landau, Institut für Informatik, Universitätsstr. 1, 56070 Koblenz, Germany, 2003.

Presented at the CADE-19 workshop Model Computation: Principles, Algorithms, Applications.

[ bib | .ps | Abstract ]

Using Mathematica and Automated Theorem Provers to Access a Mathematical Library

Ingo Dahn, Andreas Haida, Thomas Honigmann, and Christoph Wernhard

In Proceedings of the CADE-15 Workshop on Integration of Deductive Systems, pages 36-43, 1998.

(Revised and extended version: http://cs.christophwernhard.com/papers/integ.ps).

[ bib | .ps.gz | Abstract ]

First Order Proof Problems Extracted from an Article in the Mizar Mathematical Library

Ingo Dahn and Christoph Wernhard

In Maria Paola Bonacina and Ulrich Furbach, editors, International Workshop on First-Order Theorem Proving, FTP'97, RISC-Linz Report Series No. 97-50, pages 58-62. Johannes Kepler Universität, Linz, 1997.

[ bib | .ps | Abstract ]

DB-CLOS: Eine Datenbankschnittstelle für das Common Lisp Object System

Heinz Schweppe, Christoph Wernhard, and Jutta Estenfeld

In W. Remmele, editor, Künstliche Intelligenz in der Praxis. Siemens AG, 1990.

[ bib ]

Unpublished Material

InfraEngine: Inferencing in the Semantic Web by Planning

Christoph Wernhard

System description (edited 2007). (A prototype implementation can be downloaded from http://www.infraengine.com/), 2002.

[ bib | .pdf | Abstract ]

Representing Proofs in the Semantic Web

Christoph Wernhard

Working paper for Persist AG, Teltow, Germany, 2001.

[ bib | .pdf | Abstract ]

Two Short Term Applications of the Semantic Web

Christoph Wernhard

Working paper for Persist AG, Teltow, Germany, 2001.

[ bib | .pdf | Abstract ]

The Planning Web in Action

Christoph Wernhard

Working paper for Persist AG, Teltow, Germany, 2000.

[ bib | .pdf | Abstract ]

Towards a Semantic Web Modeling Language

Christoph Wernhard

Working paper for Persist AG, Teltow, Germany. Presented at KnowTech 2000, Leipzig, 2000.

[ bib | .pdf | Abstract ]

Experiments with a Linear Backward Chaining Planner

Christoph Wernhard

(Edited May 2003), 1999.

[ bib | .ps | Abstract ]

Entwurf und Implementierung einer Datenbankschnittstelle für das Common Lisp Object System

Christoph Wernhard

Magisterarbeit, Freie Universität Berlin, Berlin, Germany, 1992.

(The system documentation is available from http://cs.christophwernhard.com/closdb/.).

[ bib ]

Home Page