Importing SMT and Connection proofs as expansion trees

TL;DR

This paper introduces a method to convert SMT and Connection proof objects from different provers into a unified expansion tree format, enabling standardized analysis, validation, and manipulation of proofs.

Contribution

It presents an implementation that imports diverse proof objects into a common expansion tree framework, facilitating uniform proof analysis and validation.

Findings

Unified proof representation enables consistent analysis tools.

Proof validation is streamlined through expansion tree conversion.

Supports various proof compression and visualization techniques.

Abstract

Different automated theorem provers reason in various deductive systems and, thus, produce proof objects which are in general not compatible. To understand and analyze these objects, one needs to study the corresponding proof theory, and then study the language used to represent proofs, on a prover by prover basis. In this work we present an implementation that takes SMT and Connection proof objects from two different provers and imports them both as expansion trees. By representing the proofs in the same framework, all the algorithms and tools available for expansion trees (compression, visualization, sequent calculus proof construction, proof checking, etc.) can be employed uniformly. The expansion proofs can also be used as a validation tool for the proof objects produced.