Skip to Main content Skip to Navigation
Conference papers

Importing SMT and Connection proofs as expansion trees

Giselle Reis 1, * 
* Corresponding author
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Giselle Reis Connect in order to contact the contributor
Submitted on : Monday, October 5, 2015 - 3:04:27 PM
Last modification on : Thursday, January 20, 2022 - 5:27:40 PM
Long-term archiving on: : Wednesday, January 6, 2016 - 10:15:26 AM


Publisher files allowed on an open archive



Giselle Reis. Importing SMT and Connection proofs as expansion trees. PxTP 2015 - Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, Aug 2015, Berlin, Germany. ⟨10.4204/EPTCS.186.3⟩. ⟨hal-01208325⟩



Record views


Files downloads