Home Page

Papers

Publications

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 | http | 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, LNCS (LNAI). Springer, 2017.
To appear [ Preprint ].
bib | Abstract ]

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), number 1635 in CEUR Workshop Proceedings, pages 125-138, Aachen, 2016.
bib | http | 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.
bib | .pdf | 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 176-179. nisaba verlag, 2016.
bib | .pdf ]

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.
bib | .pdf | 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.
bib | 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.
bib | 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.
bib | 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 (Manuscript: http://cs.christophwernhard.com/papers/inprocessing.pdf).
bib | 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.
bib | Abstract ]

Projection and Scope-Determined Circumscription
Christoph Wernhard
Journal of Symbolic Computation, 47:1089-1108, 2012.
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 | http | 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.
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.
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.
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.
bib | DOI | Abstract ]

System Description: E-KRHyper
Björn Pelzer and Christoph Wernhard
In Frank Pfennig, 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 | .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 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/cdb/.).
bib ]

Home Page