Importing SMT and Connection proofs as expansion trees

Giselle Reis 1, *
* Auteur correspondant
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.
Type de document :
Communication dans un congrès
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2015, Berlin, Germany. 2015, 〈10.4204/EPTCS.186.3〉
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01208325
Contributeur : Giselle Reis <>
Soumis le : lundi 5 octobre 2015 - 15:04:27
Dernière modification le : samedi 18 février 2017 - 01:14:40
Document(s) archivé(s) le : mercredi 6 janvier 2016 - 10:15:26

Fichier

1507.08715v1.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

48

Téléchargements de fichiers

38