Ordered Resolution with Straight Dismatching Constraints

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 : lundi 20 novembre 2017 - 15:14:02
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

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〉

Partager

Métriques

Consultations de la notice

88

Téléchargements de fichiers

14