1 citations · 2 across the 3 of their papers we have counts for
5 papers · 1 filter
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.…
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…
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…
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…