research
∙
06/06/2023
Range-Restricted Interpolation through Clausal Tableaux
We show how variations of range-restriction and also the Horn property c...
share
research
∙
03/10/2023
Lemmas: Generation, Selection, Application
Noting that lemmas are a key feature of mathematics, we engage in an inv...
research
∙
02/14/2023
Investigations into Proof Structures
We introduce and elaborate a novel formalism for the manipulation and an...
research
∙
12/06/2022
Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
Derived datasets can be defined implicitly or explicitly. An implicit de...
research
∙
09/26/2022
Generating Compressed Combinatory Proof Structures – An Approach to Automated First-Order Theorem Proving
Representing a proof tree by a combinator term that reduces to the tree ...
research
∙
09/17/2022
Synthesizing Nested Relational Queries from Implicit Specifications
Derived datasets can be defined implicitly or explicitly. An implicit de...
research
∙
07/18/2022
CD Tools – Condensed Detachment and Structure Generating Theorem Proving (System Description)
CD Tools is a Prolog library for experimenting with condensed detachment...
research
∙
10/21/2021
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
In recent years, Gödel's ontological proof and variations of it were for...
research
∙
04/28/2021
Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)
The material presented in this paper contributes to establishing a basis...
research
∙
08/08/2020
Craig Interpolation with Clausal First-Order Tableaux
We develop foundations for computing Craig-Lyndon interpolants of two gi...
research
∙
02/24/2020
Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
PIE is a Prolog-embedded environment for automated reasoning on the basi...
research
∙
02/24/2020
KBSET – Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative LaTeX Markup and a Core Written in SWI-Prolog
KBSET is an environment that provides support for scholarly editing in t...
research
∙
08/29/2019
PIE – Proving, Interpolating and Eliminating on the Basis of First-Order Logic
PIE is a Prolog-embedded environment for automated reasoning on the basi...
research
∙
08/29/2019
KBSET -- Knowledge-Based Support for Scholarly Editing and Text Processing
KBSET supports a practical workflow for scholarly editing, based on usin...
research
∙
02/14/2018
Craig Interpolation and Access Interpolation with Clausal First-Order Tableaux
We show methods to extract Craig-Lyndon interpolants and access interpol...
research
∙
12/19/2017
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
For relational monadic formulas (the Löwenheim class) second-order quant...
research
∙
06/26/2017
The Boolean Solution Problem from the Perspective of Predicate Logic - Extended Version
Finding solution values for unknowns in Boolean equations was a principa...
research
∙
08/24/2011