Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Wednesday, September 20, 2017 - 11:35:33 AM
Last modification on : Wednesday, November 3, 2021 - 7:09:41 AM


Files produced by the author(s)


  • HAL Id : hal-01590782, version 1



Serdar Erbatur, Andrew 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⟩



Les métriques sont temporairement indisponibles