Christoph Wernhard

62 papers A* 1A 3B 6Journal 29Unranked 18

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Craig Interpolation for HT with a Variation of Mints' Sequent System. CoRR Christoph Wernhard
2026	J	`jnl`	Generating Theorems by Generating Proof Structures. CoRR Christoph Wernhard
2025	J	`jnl`	Interpolation in Classical Propositional Logic. CoRR Patrick Koopmann, Christoph Wernhard, Frank Wolter
2025	J	`jnl`	Interpolation with Automated First-Order Reasoning. CoRR Christoph Wernhard
2025	J	`jnl`	Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures. CoRR Christoph Wernhard, Zsolt Zombori
2024	J	`jnl`	Investigations into Proof Structures. J. Autom. Reason. Christoph Wernhard, Wolfgang Bibel
2024	—	`conf`	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic. IJCAR (1) Jan Heuer, Christoph Wernhard
2024	J	`jnl`	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic. CoRR Jan Heuer, Christoph Wernhard
2024	J	`jnl`	Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory. Log. Methods Comput. Sci. Michael Benedikt, Cécilia Pradic, Christoph Wernhard
2023	J	`jnl`	Investigations into Proof Structures. CoRR Christoph Wernhard, Wolfgang Bibel
2023	B	`conf`	Lemmas: Generation, Selection, Application. TABLEAUX Michael Rawson, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel
2023	J	`jnl`	Lemmas: Generation, Selection, Application. CoRR Michael Rawson, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel
2023	J	`jnl`	Range-Restricted Interpolation through Clausal Tableaux. CoRR Christoph Wernhard
2023	B	`conf`	Range-Restricted and Horn Interpolation through Clausal Tableaux. TABLEAUX Christoph Wernhard
2023	—	`conf`	Structure-Generating First-Order Theorem Proving. AReCCa@TABLEAUX Christoph Wernhard
2023	A*	`conf`	Synthesizing Nested Relational Queries from Implicit Specifications. PODS Michael Benedikt, Cécilia Pradic, Christoph Wernhard
2022	J	`jnl`	CD Tools - Condensed Detachment and Structure Generating Theorem Proving (System Description). CoRR Christoph Wernhard
2022	J	`jnl`	Generating Compressed Combinatory Proof Structures - An Approach to Automated First-Order Theorem Proving. CoRR Christoph Wernhard
2022	—	`conf`	Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving. PAAR@IJCAR Christoph Wernhard
2022	J	`jnl`	Synthesizing Nested Relational Queries from Implicit Specifications. CoRR Michael Benedikt, Cécilia Pradic, Christoph Wernhard
2022	J	`jnl`	Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory. CoRR Michael Benedikt, Cécilia Pradic, Christoph Wernhard
2021	—	`conf`	Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof. SOQE@KR Christoph Wernhard
2021	J	`jnl`	Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof. CoRR Christoph Wernhard
2021	J	`jnl`	Craig Interpolation with Clausal First-Order Tableaux. J. Autom. Reason. Christoph Wernhard
2021	J	`jnl`	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version). CoRR Christoph Wernhard, Wolfgang Bibel
2021	A	`conf`	Learning from Łukasiewicz and Meredith: Investigations into Proof Structures. CADE Christoph Wernhard, Wolfgang Bibel
2021	—	`ed.`	Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2021) associated with the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021), Online Event, November 4, 2021. SOQE@KR Renate A. Schmidt, Christoph Wernhard, Yizheng Zhao
2020	J	`jnl`	Craig Interpolation with Clausal First-Order Tableaux. CoRR Christoph Wernhard
2020	J	`jnl`	Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic. CoRR Christoph Wernhard
2020	J	`jnl`	KBSET - Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative LaTeX Markup and a Core Written in SWI-Prolog. CoRR Jana Kittelmann, Christoph Wernhard
2019	—	`conf`	Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic. DECLARE Christoph Wernhard
2019	—	`conf`	KBSET - Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative LaTeX Markup and a Core Written in SWI-Prolog. DECLARE Jana Kittelmann, Christoph Wernhard
2019	J	`jnl`	KBSET - Knowledge-Based Support for Scholarly Editing and Text Processing. CoRR Jana Kittelmann, Christoph Wernhard
2019	J	`jnl`	PIE - Proving, Interpolating and Eliminating on the Basis of First-Order Logic. CoRR Christoph Wernhard
2018	J	`jnl`	Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux. CoRR Christoph Wernhard
2017	—	`conf`	Approximating Resultants of Existential Second-Order Quantifier Elimination upon Universal Relational First-Order Formulas. SOQE Christoph Wernhard
2017	—	`conf`	Early Steps of Second-Order Quantifier Elimination beyond the Monadic Case: The Correspondence between Heinrich Behmann and Wilhelm Ackermann 1928-1934 (Abstract). SOQE Christoph Wernhard
2017	J	`jnl`	Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic. CoRR Christoph Wernhard
2017	—	`ed.`	Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), Dresden, Germany, December 6-8, 2017. SOQE Patrick Koopmann, Sebastian Rudolph, Renate A. Schmidt, Christoph Wernhard
2017	—	`conf`	The Boolean Solution Problem from the Perspective of Predicate Logic (Abstract). SOQE Christoph Wernhard
2017	J	`jnl`	The Boolean Solution Problem from the Perspective of Predicate Logic - Extended Version. CoRR Christoph Wernhard
2017	—	`conf`	The Boolean Solution Problem from the Perspective of Predicate Logic. FroCoS Christoph Wernhard
2017	—	`ed.`	YSIP2 - Proceedings of the Second Young Scientist's International Workshop on Trends in Information Processing, Dombai, Russian Federation, May 16-20, 2017. YSIP Steffen Hölldobler, Andrey Malikov, Christoph Wernhard
2016	—	`conf`	Knowledge-Based Support for Scholarly Editing and Text Processing. DHd Jana Kittelmann, Christoph Wernhard
2016	—	`conf`	The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating. PAAR@IJCAR Christoph Wernhard
2015	B	`conf`	Second-Order Quantifier Elimination on Relational Monadic Formulas - A Basic Method and Some Less Expected Applications. TABLEAUX Christoph Wernhard
2014	J	`jnl`	Modeling the suppression task under weak completion and well-founded semantics. J. Appl. Non Class. Logics Emmanuelle-Anna Dietz, Steffen Hölldobler, Christoph Wernhard
2014	—	`ed.`	Proceedings of the Young Scientists' International Workshop on Trends in Information Processing (YSIP) Co-located with the Sixth International Conference on Infocommunicational Technologies in Science, Production and Education (INFOCOM-6), Stavropol, Russian Federation, April 22-25, 2014. YSIP Steffen Hölldobler, Andrey Malikov, Christoph Wernhard
2013	—	`conf`	Abduction in Logic Programming as Second-Order Quantifier Elimination. FroCos Christoph Wernhard
2013	A	`conf`	Soundness of Inprocessing in Clause Sharing SAT Solvers. SAT Norbert Manthey, Tobias Philipp, Christoph Wernhard
2012	J	`jnl`	Projection and scope-determined circumscription. J. Symb. Comput. Christoph Wernhard
2011	—	`conf`	An Abductive Model for Human Reasoning. AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning Steffen Hölldobler, Tobias Philipp, Christoph Wernhard
2011	J	`jnl`	Computing with Logic as Operator Elimination: The ToyElim System CoRR Christoph Wernhard
2011	—	`conf`	Computing with Logic as Operator Elimination: The ToyElim System. INAP/WLP Christoph Wernhard
2010	—	`conf`	Circumscription and Projection as Primitives of Logic Programming. ICLP (Technical Communications) Christoph Wernhard
2009	—	`—`	Automated deduction for projection elimination. Christoph Wernhard
2009	—	`conf`	Literal Projection and Circumscription. FTP Christoph Wernhard
2009	B	`conf`	Tableaux for Projection Computation and Knowledge Compilation. TABLEAUX Christoph Wernhard
2008	B	`conf`	Literal Projection for First-Order Logic. JELIA Christoph Wernhard
2007	A	`conf`	System Description: E-KRHyper. CADE Björn Pelzer, Christoph Wernhard
2004	—	`conf`	Semantic Knowledge Partitioning. IJCAR Doctoral Programme Christoph Wernhard
2004	B	`conf`	Semantic Knowledge Partitioning. JELIA Christoph Wernhard