Papers
Investigations into Proof Structures
Christoph Wernhard and Wolfgang Bibel
Journal of Automated Reasoning, 68(24), 2024.
Exploring Metamath Proof Structures (Extended Abstract)
Christoph Wernhard and Zsolt Zombori
In Michael R. Douglas, Thomas C. Hales, Cezary Kaliszyk, Stephan
Schulz, and Josef Urban, editors, 9th Conference on Artificial
Intelligence and Theorem Proving, AITP 2024 (Informal Book of Abstracts),
2024.
Forward Reasoning in Hindsight (Project Proposal)
Michael Rawson, Zsolt Zombori, Maximilian Doré, and Christoph Wernhard
In Michael R. Douglas, Thomas C. Hales, Cezary Kaliszyk, Stephan
Schulz, and Josef Urban, editors, 9th Conference on Artificial
Intelligence and Theorem Proving, AITP 2024 (Informal Book of Abstracts),
2024.
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, 20(3), 2024.
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,
volume 14739 of LNCS (LNAI), pages 172-193. Springer, 2024.
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.
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.
Lemmas: Generation, Selection, Application
Michael Rawson, Christoph Wernhard, Zsolt Zombori, and Wolfgang Bibel
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
153-174. Springer, 2023.
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.
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.
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.
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.
CD Tools - Condensed Detachment and Structure Generating Theorem
Proving (System Description)
Christoph Wernhard
Technical report, 2022.
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.
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.
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.
Craig Interpolation with Clausal First-Order Tableaux
Christoph Wernhard
Journal of Automated Reasoning, 65(5):647-690, 2021.
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.
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
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 178-196. Springer, 2020.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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 ].
Application Patterns of Projection/Forgetting
Christoph Wernhard
Workshop presentation [
Slides ].
Second-Order Characterizations of Definientia in Formula Classes
Christoph Wernhard
Technical Report Knowledge Representation and Reasoning 14-03,
Technische Universität Dresden, 2014.
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.
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.
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.
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.
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.
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.
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.
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 ].
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.
Projection and Scope-Determined Circumscription
Christoph Wernhard
Journal of Symbolic Computation, 47:1089-1108, 2012.
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.
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.
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.
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.
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.
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.
Automated Deduction for Projection Elimination
Christoph Wernhard
Number 324 in Dissertations in Artificial Intelligence. AKA
Verlag/IOS Press, Heidelberg, Amsterdam, 2009.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
InfraEngine: Inferencing in the Semantic Web by Planning
Christoph Wernhard
Representing Proofs in the Semantic Web
Christoph Wernhard
Working paper for Persist AG, Teltow, Germany, 2001.
Two Short Term Applications of the Semantic Web
Christoph Wernhard
Working paper for Persist AG, Teltow, Germany, 2001.
The Planning Web in Action
Christoph Wernhard
Working paper for Persist AG, Teltow, Germany, 2000.
Towards a Semantic Web Modeling Language
Christoph Wernhard
Working paper for Persist AG, Teltow, Germany. Presented at
KnowTech 2000, Leipzig, 2000.
Experiments with a Linear Backward Chaining Planner
Christoph Wernhard
(Edited May 2003), 1999.
Entwurf und Implementierung einer Datenbankschnittstelle
für das Common Lisp Object System
Christoph Wernhard
Magisterarbeit, Freie Universität Berlin, Berlin, Germany, 1992.