Semantic Knowledge Partitioning. - Christoph Wernhard (JELIA, 2004)

System Description: E-KRHyper. - Björn Pelzer; Christoph Wernhard (CADE, 2007)

Literal Projection for First-Order Logic. - Christoph Wernhard (JELIA, 2008)

Literal Projection and Circumscription. - Christoph Wernhard (FTP, 2009)

Tableaux for Projection Computation and Knowledge Compilation. - Christoph Wernhard (TABLEAUX, 2009)

Automated deduction for projection elimination. - Christoph Wernhard (2009)

Circumscription and Projection as Primitives of Logic Programming. - Christoph Wernhard (ICLP (Technical Communications), 2010)

An Abductive Model for Human Reasoning. - Steffen Hölldobler; Tobias Philipp; Christoph Wernhard (AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning, 2011)

Computing with Logic as Operator Elimination: The ToyElim System. - Christoph Wernhard (INAP/WLP, 2011)

Projection and scope-determined circumscription. - Christoph Wernhard (J. Symb. Comput., 2012)

Abduction in Logic Programming as Second-Order Quantifier Elimination. - Christoph Wernhard (FroCos, 2013)

Soundness of Inprocessing in Clause Sharing SAT Solvers. - Norbert Manthey; Tobias Philipp; Christoph Wernhard (SAT, 2013)

Modeling the suppression task under weak completion and well-founded semantics. - Emmanuelle-Anna Dietz; Steffen Hölldobler; Christoph Wernhard (J. Appl. Non Class. Logics, 2014)

Second-Order Quantifier Elimination on Relational Monadic Formulas - A Basic Method and Some Less Expected Applications. - Christoph Wernhard (TABLEAUX, 2015)

The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating. - Christoph Wernhard (PAAR@IJCAR, 2016)

Knowledge-Based Support for Scholarly Editing and Text Processing. - Jana Kittelmann; Christoph Wernhard (DHd, 2016)

The Boolean Solution Problem from the Perspective of Predicate Logic. - Christoph Wernhard (FroCoS, 2017)

Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas. - Christoph Wernhard (SOQE, 2017)

The Boolean Solution Problem from the Perspective of Predicate Logic (Abstract). - Christoph Wernhard (SOQE, 2017)

Early Steps of Second-Order Quantifier Elimination beyond the Monadic Case: The Correspondence between Heinrich Behmann and Wilhelm Ackermann 1928-1934 (Abstract). - Christoph Wernhard (SOQE, 2017)

The Boolean Solution Problem from the Perspective of Predicate Logic - Extended Version. - Christoph Wernhard (CoRR, 2017)

Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic. - Christoph Wernhard (CoRR, 2017)

Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux. - Christoph Wernhard (CoRR, 2018)

KBSET - Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative [inline-graphic not available: see fulltext] Markup and a Core Written in SWI-Prolog. - Jana Kittelmann; Christoph Wernhard (DECLARE, 2019)

Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic. - Christoph Wernhard (DECLARE, 2019)

KBSET - Knowledge-Based Support for Scholarly Editing and Text Processing. - Jana Kittelmann; Christoph Wernhard (CoRR, 2019)

PIE - Proving, Interpolating and Eliminating on the Basis of First-Order Logic. - Christoph Wernhard (CoRR, 2019)

KBSET - Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative LaTeX Markup and a Core Written in SWI-Prolog. - Jana Kittelmann; Christoph Wernhard (CoRR, 2020)

Learning from Łukasiewicz and Meredith: Investigations into Proof Structures. - Christoph Wernhard; Wolfgang Bibel (CADE, 2021)

Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof. - Christoph Wernhard (SOQE@KR, 2021)

Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version). - Christoph Wernhard; Wolfgang Bibel (CoRR, 2021)

Craig Interpolation with Clausal First-Order Tableaux. - Christoph Wernhard (J. Autom. Reason., 2021)

Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving. - Christoph Wernhard (PAAR@IJCAR, 2022)

CD Tools - Condensed Detachment and Structure Generating Theorem Proving (System Description). - Christoph Wernhard (CoRR, 2022)

Structure-Generating First-Order Theorem Proving. - Christoph Wernhard (AReCCa@TABLEAUX, 2023)

Synthesizing Nested Relational Queries from Implicit Specifications. - Michael Benedikt; Cécilia Pradic; Christoph Wernhard (PODS, 2023)

Lemmas: Generation, Selection, Application. - Michael Rawson 001; Christoph Wernhard; Zsolt Zombori; Wolfgang Bibel (TABLEAUX, 2023)

Range-Restricted and Horn Interpolation through Clausal Tableaux. - Christoph Wernhard (TABLEAUX, 2023)

Range-Restricted Interpolation through Clausal Tableaux. - Christoph Wernhard (CoRR, 2023)

Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic. - Jan Heuer; Christoph Wernhard (IJCAR (1), 2024)

Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory. - Michael Benedikt; Cécilia Pradic; Christoph Wernhard (Log. Methods Comput. Sci., 2024)

Investigations into Proof Structures. - Christoph Wernhard; Wolfgang Bibel (J. Autom. Reason., 2024)

Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures. - Christoph Wernhard; Zsolt Zombori (CoRR, 2025)

Interpolation with Automated First-Order Reasoning. - Christoph Wernhard (CoRR, 2025)