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.

Connecting many-sorted theories / Franz Baader, Silvio Ghilardi - In: Automated Deduction – CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : Proceedings / Robert Nieuwenhuis. - Berlin : Springer, 2005. - ISBN 3540280057. - pp. 278-294 (( Intervento presentato al 20. convegno International Conference on Automated Deduction (CADE-20) tenutosi a Tallinn nel 2005.

Connecting many-sorted theories

Silvio Ghilardi
2005

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.
Combination, E-connections.
Settore M-FIL/02 - Logica e Filosofia della Scienza
2005
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/5518
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? ND
social impact