A Flexible Proof Format for SMT: a Proposal - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

A Flexible Proof Format for SMT: a Proposal

(1) , (2) , (3)


The standard input format for Satisfiability Modulo Theories (SMT) solvers has now reached its second version and integrates many of the features useful for users to interact with their favourite SMT solver. However, although many SMT solvers do output proofs, no standardised proof format exists. We, here, propose for discussion at the PxTP Workshop a generic proof format in the SMT-LIB philosophy that is flexible enough to be easily recast for any SMT solver. The format is configurable so that the proof can be provided by the solver at the desired level of detail.
Fichier principal
Vignette du fichier
paper3.pdf (103.64 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-00642544 , version 1 (07-03-2012)


  • HAL Id : hal-00642544 , version 1


Frédéric Besson, Pascal Fontaine, Laurent Théry. A Flexible Proof Format for SMT: a Proposal. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. ⟨hal-00642544⟩
9015 View
161 Download


Gmail Facebook Twitter LinkedIn More