Skip to Main content Skip to Navigation
New interface
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
Contributor : Pascal Fontaine Connect in order to contact the contributor
Submitted on : Wednesday, March 7, 2012 - 3:28:39 PM
Last modification on : Friday, February 4, 2022 - 3:25:12 AM
Long-term archiving on: : Friday, November 23, 2012 - 4:00:27 PM


Files produced by the author(s)


  • HAL Id : hal-00642535, version 1



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⟩



Record views


Files downloads