Proofs as Formal Objects and as Data
– Project Page –
The project is in the area of automated reasoning, a central subfield
of Artificial Intelligence, whose topic is the investigation of
reasoning by means of the computer. Typical automated reasoning systems
create proof structures: representations of proofs, combined deduction
steps, as data structures. Proof structures can be understood on the one
hand as formal objects that are related in specific ways to logical
formulas, and, on the other hand, as data objects that materialize these
formal objects and can be used for practical applications. Starting out
from the investigation of proof structures in this sense, the project
aims at both, improving the capability of automated reasoning systems to
find proofs, and extending the range of tasks that can be solved by
them, beyond theorem proving in the strict sense.
Aside of the interplay of theoretical and experimental methods that
characterizes the field of automated reasoning, a specific methodical
aspect of the project is the analysis of given proofs. Of particular
relevance is there an extensive corpus of advanced formal proofs from
the literature before the broad availability of computers, which still
can not be found in a satisfactory way by automated methods.
The specific objectives of the project are:
- Improving the capability of first-order theorem provers to find
proofs, in particular through novel calculi, guided by abstractions
emerging from the orientation at proof structures and by
observations made in the analysis of proofs.
- Theoretically well-understood and implemented proof
transformations for various practical applications, such as
shortening or simplification of proofs, discovery and abstraction of
repetitions and regularities in proofs, or mappings between calculi
to enable the combination of different systems.
- Applicability of automated reasoning to query reformulation for
integrating data and knowledge bases as well as query optimization.
It is planned to refine and extend an approach to query
reformulation that is based on Craig interpolation, a fundamental
relationship in first-order logic between proof structures and
- Progress in certain advanced issues of theoretical and practical
interest that are related to the core techniques considered in the
project, Craig interpolation and condensed detachment. The latter is
the primary proof representation in the analyzed literature. Goals
are in particular the overcoming of known limitations, insights into
relationships to further techniques, and availability of further
from Łukasiewicz and Meredith: Investigations into Proof
In André Platzer and Geoff Sutcliffe,
editors, Automated Deduction: CADE 2021, volume 12699 of LNCS
(LNAI), pages 58-75. Springer, 2021.
Interpolation with Clausal First-Order
Journal of Automated