Christoph Wernhard

Michael Rawson, Christoph Wernhard, Zsolt Zombori et al.

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 combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.

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-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to Łukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of Łukasiewicz's problem was automatically discovered that is much shorter than any proof found before by man or machine.

Christoph Wernhard

We consider interpolation from the viewpoint of fully automated theorem proving in first-order logic as a general core technique for mechanized knowledge processing. For Craig interpolation, our focus is on the two-stage approach, where first an essentially propositional ground interpolant is calculated that is then lifted to a quantified first-order formula. We discuss two possibilities to obtain a ground interpolant from a proof: with clausal tableaux, and with resolution. Established preprocessing techniques for first-order proving can also be applied for Craig interpolation if they are restricted in specific ways. Equality encodings from automated reasoning justify strengthened variations of Craig interpolation. Contributions to Craig interpolation that emerged from automated reasoning include variations for logics used in databases and logic programming. As an approach to uniform interpolation we introduce second-order quantifier elimination with examples and describe the basic algorithms DLS and SCAN.

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 tableaux, which stems from first-order ATP. Our results are induced by a restriction of the clausal tableau structure, which can be achieved in general by a proof transformation, also if the source proof is by resolution/paramodulation. Primarily addressed applications are query synthesis and reformulation with interpolation. Our methodical approach combines operations on proof structures with the immediate perspective of feasible implementation through incorporating highly optimized first-order provers.

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 in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)". The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by Łukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.