Quantifier Inference Rules for SMT proofs

Abstract : This paper discusses advantages and disadvantages of some possible alternatives for inference rules that handle quantifiers in the proof format of the SMT-solver veriT. The quantifier-handling modules in veriT being fairly standard, we hope this will motivate the discussion among the PxTP audience around proof production for quantifier handling. This could generate ideas to help us improve our proof production module, and also benefit the SMT community.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-00642535
Contributor : Pascal Fontaine <>
Submitted on : Wednesday, March 7, 2012 - 3:28:39 PM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM
Document(s) archivé(s) le : Friday, November 23, 2012 - 4:00:27 PM

File

paper2.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00642535, version 1

Collections

Citation

David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo. Quantifier Inference Rules for SMT proofs. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. ⟨hal-00642535⟩

Share

Metrics

Record views

645

Files downloads

184