11 citations · 47 across the 17 of their papers we have counts for
Showing 2023Show all
3 papers · 1 filter
cs.LO2023★ 3 cited
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…
cs.LO2023★ 3 cited
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-…
cs.LO2023★ 5 cited
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…