Non-Disjoint Combination with Forward-Closed Theories

International audienceWe consider the class of forward-closed theories defined as theequational theories generated by forward-closed convergent rewritesystems. In this particular class of syntactic theories, theunification problem can be solved thanks to a mutation-basedunification algorithm. This is shown by reusing an approach based onBasic Syntactic Mutation originally developed for equational theoriessaturated by paramodulation. Then this mutation-based algorithm isapplied in a new combination algorithm that solves the unificationproblem in some non-disjoint extensions of forward-closed theories