Combining Equational Theories Sharing Non-Collapse-Free Constructors

In this paper we extend the applicability of our combination method for decision procedures for the word problem to theories sharing non-collapse-free constructors. This extension broadens the scope of the combination procedure considerably, for example in the direction of equational theories axiomatizing the equivalence of modal formulae.

• Type: Conference
• Year: 2000
• Where: FROCOS
• Authors: Franz Baader, Cesare Tinelli
• Keywords: Combination Method, Combination Procedure, Control Systems, Decision Procedures, FROCOS 2000