Skip to Main content Skip to Navigation
Conference papers

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
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-00642535
Contributor : Pascal Fontaine Connect in order to contact the contributor
Submitted on : Wednesday, March 7, 2012 - 3:28:39 PM
Last modification on : Saturday, October 16, 2021 - 11:26:10 AM
Long-term archiving on: : 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

779

Files downloads

262