Non-Disjoint Combination with Forward-Closed Theories

Abstract : We consider the class of forward-closed theories defined as the equational theories generated by forward-closed convergent rewrite systems. In this particular class of syntactic theories, the unification problem can be solved thanks to a mutation-based unification algorithm. This is shown by reusing an approach based on Basic Syntactic Mutation originally developed for equational theories saturated by paramodulation. Then this mutation-based algorithm is applied in a new combination algorithm that solves the unification problem in some non-disjoint extensions of forward-closed theories.
Type de document :
Communication dans un congrès
31th International Workshop on Unification, UNIF 2017, Sep 2017, Oxford, United Kingdom
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01590782
Contributeur : Christophe Ringeissen <>
Soumis le : mercredi 20 septembre 2017 - 11:35:33
Dernière modification le : jeudi 11 janvier 2018 - 06:27:43

Fichier

combi-bs-unif.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01590782, version 1

Citation

Serdar Erbatur, Andrew Marshall, Christophe Ringeissen. Non-Disjoint Combination with Forward-Closed Theories. 31th International Workshop on Unification, UNIF 2017, Sep 2017, Oxford, United Kingdom. 〈hal-01590782〉

Partager

Métriques

Consultations de la notice

84

Téléchargements de fichiers

24