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…