11 citations · 47 across the 17 of their papers we have counts for
17 papers
Range-Restricted Interpolation through Clausal Tableaux
Christoph Wernhard
We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig interpolation in first-order logic. The proof system is clausal…
Investigations into Proof Structures
Christoph Wernhard, Wolfgang Bibel
We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-…
Lemmas: Generation, Selection, Application
Michael Rawson, Christoph Wernhard, Zsolt Zombori +1
Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combin…
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving
Christoph Wernhard
Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term.…
Synthesizing Nested Relational Queries from Implicit Specifications
Michael Benedikt, Cécilia Pradic, Christoph Wernhard
Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset in terms of datasets ) is a logical specification involving the source dat…
CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)
Christoph Wernhard
CD Tools is a Prolog library for experimenting with condensed detachment in first-order ATP, which puts a recent formal view centered around proof structures into practice. From th…
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
Christoph Wernhard
In recent years, Gödel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in a…
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)
Christoph Wernhard, Wolfgang Bibel
The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features…
Craig Interpolation with Clausal First-Order Tableaux
Christoph Wernhard
We develop foundations for computing Craig-Lyndon interpolants of two given formulas with first-order theorem provers that construct clausal tableaux. Provers that can be understoo…
Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
Christoph Wernhard
PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. Its main focus is on formulas, as constituents of complex formalizations that are st…
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
KBSET is an environment that provides support for scholarly editing in two flavors: First, as a practical tool KBSET/Letters that accompanies the development of editions of corresp…
PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic
Christoph Wernhard
PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It includes a versatile formula macro system and supports the creation of documents…
KBSET -- Knowledge-Based Support for Scholarly Editing and Text Processing
Jana Kittelmann, Christoph Wernhard
KBSET supports a practical workflow for scholarly editing, based on using LaTeX with dedicated commands for semantics-oriented markup and a Prolog-implemented core system. Prolog p…
Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux
Christoph Wernhard
We develop foundations for computing Craig interpolants and similar intermediates of two given formulas with first-order theorem provers that construct clausal tableaux. Provers th…
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
Christoph Wernhard
For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, projection and forgettin…
The Boolean Solution Problem from the Perspective of Predicate Logic -- Extended Version
Christoph Wernhard
Finding solution values for unknowns in Boolean equations was a principal reasoning mode in the Algebra of Logic of the 19th century. Schröder investigated it as Auflösungsproblem…
Computing with Logic as Operator Elimination: The ToyElim System
Christoph Wernhard
A prototype system is described whose core functionality is, based on propositional logic, the elimination of second-order operators, such as Boolean quantifiers and operators for…