Ordered Resolution with Straight Dismatching Constraints

Andreas Teucke 1 Christoph Weidenbach 2, 1
1 MPII - Max-Planck-Institut für Informatik
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We present a sound and complete ordered resolution calculus for first-order clauses with straight dismatching constraints. The extended clause language is motivated by our first-order theorem proving approach through approximation and refinement. Using a clause language with straight dismatching constraints, single refinement steps do not result in a worst-case quadratic blowup in the number of clauses anymore. The refinement steps can now be represented by replacing one input clause with two equivalent clauses. We show soundness and completeness of ordered resolution with straight dismatching constraints. All needed operations on straight dismatching constraints take linear or linear logarithmic time in the size of the constraint.
Type de document :
Communication dans un congrès
Pascal Fontaine and Stephan Schulz and Josef Urban. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), 2016, Coimbra, Portugal. 1635, pp.95-109, 2016, CEUR Workshop Proceedings
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01403206
Contributeur : Stephan Merz <>
Soumis le : lundi 28 novembre 2016 - 16:53:35
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : mardi 21 mars 2017 - 09:42:59

Fichier

paar.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : hal-01403206, version 1

Collections

INRIA | LORIA | LORIA-FM | UNIV-LORRAINE

Citation

Andreas Teucke, Christoph Weidenbach. Ordered Resolution with Straight Dismatching Constraints. Pascal Fontaine and Stephan Schulz and Josef Urban. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), 2016, Coimbra, Portugal. 1635, pp.95-109, 2016, CEUR Workshop Proceedings. 〈hal-01403206〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

141

Téléchargements de fichiers

24

Contact


archive-ouverte@inria.fr