Integrating Simplex with Tableaux

Abstract : We propose an extension of a tableau-based calculus to deal with linear arithmetic. This extension consists of a smooth integration of arithmetic deductive rules to the basic tableau rules, so that there is a natural interleaving between arithmetic and regular analytic rules. The arithmetic rules rely on the general simplex algorithm to compute solutions for systems over rationals, as well as on the branch and bound method to deal with integer systems. We also describe our implementation in the framework of Zenon, an automated theorem prover that is able to deal with first order logic with equality. This implementation has been provided with a backend verifier that relies on the Coq proof assistant , and which can verify the validity of the generated arithmetic proofs. Finally, we present some experimental results over the arithmetic category of the TPTP library, and problems of program verification coming from the benchmark provided by the BWare project.
Type de document :
Communication dans un congrès
Hans de Nivelle. Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wrowlaw, Poland. Lecture notes in computer science, pp.86-101, 2015, 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. 〈10.1007/978-3-319-24312-2_7〉
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-01215490
Contributeur : Guillaume Bury <>
Soumis le : mercredi 14 octobre 2015 - 12:40:50
Dernière modification le : mardi 13 novembre 2018 - 17:10:03
Document(s) archivé(s) le : jeudi 27 avril 2017 - 04:47:53

Fichier

zen-ari.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Guillaume Bury, David Delahaye. Integrating Simplex with Tableaux. Hans de Nivelle. Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wrowlaw, Poland. Lecture notes in computer science, pp.86-101, 2015, 24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. 〈10.1007/978-3-319-24312-2_7〉. 〈hal-01215490〉

Partager

Métriques

Consultations de la notice

163

Téléchargements de fichiers

135