Connecting Many-Sorted Theories

Abstract. Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions under which decidability of the validity of universal formulae in the component theories transfers to their connection. In addition, we consider variants of the basic connection scheme.

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Franz Baader, Silvio Ghilardi
• Keywords: Automated Reasoning, Basic Connection Scheme, CADE 2005, Component Theories, Connection Functions