Non-Disjoint Combination with Forward-Closed Theories - Archive ouverte HAL Access content directly
Conference Papers Year :

Non-Disjoint Combination with Forward-Closed Theories

(1) , (2) , (3)
1
2
3
Serdar Erbatur
  • Function : Author
  • PersonId : 1016941
Andrew M. Marshall
  • Function : Author
  • PersonId : 1016942

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.
Fichier principal
Vignette du fichier
combi-bs-unif.pdf (271.77 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01590782 , version 1 (20-09-2017)

Identifiers

  • HAL Id : hal-01590782 , version 1

Cite

Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen. Non-Disjoint Combination with Forward-Closed Theories. 31th International Workshop on Unification, UNIF 2017, Adrià Gascón; Christopher Lynch, Sep 2017, Oxford, United Kingdom. ⟨hal-01590782⟩
75 View
27 Download

Share

Gmail Facebook Twitter LinkedIn More