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.
Type de document :
Communication dans un congrès
Pascal Fontaine and Aaron Stump. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. 2011
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00642535
Contributeur : Pascal Fontaine <>
Soumis le : mercredi 7 mars 2012 - 15:28:39
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25
Document(s) archivé(s) le : vendredi 23 novembre 2012 - 16:00:27

Fichier

paper2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00642535, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

287

Téléchargements de fichiers

160