Recent Advances in Combined Decision Problems
Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli · 2006
Questo articolo vuol essere un’esposizione aggiornata, benché necessaria-mente parziale, dello stato dell’arte della ricerca relativa all’integrazione modulare di procedure di decisione nella logica elementare. Nello specifico, date due teorie T1 e T2 il cui frammento universale è decidibile, si è inte-ressati ad individuare quali siano le condizioni che permettono di trasferire tale decidibilità alla teoria ottenuta dall’unione di T1 e T2. Allo scopo di dare un quadro il più possibile completo ed approfondito delle ricerche in questo campo, vengono presentati anche risultati sulla possibilità di tra-sferire alla teoria unione la decidibilità del problema della parola e viene descritto un ambiente di ordine superiore in cui esprimere svariati problemi di combinazione. Infine, viene fornita la descrizione ad alto livello di alcune delle tecniche più comunemente utilizzate nell’implementazione di efficienti sistemi per la combinazione. Many areas of computer science (like software and hardware verification, artifi-cial intelligence, knowledge representation and even computational algebra) are interested in the study and in the development of combination and integration techniques for existing decision procedures: this is so because there is a need to reason in heterogeneous domains, so that modularity in combining and re-using algorithms and concrete implementations becomes crucial. In this paper we consider two decision problems: first, given a first-order theory T in a signature Σ,1 the word problem for T is that of deciding whether T | = t = u holds for the Σ-terms t and u. Second, the constraint satisfiability problem for T is the problem of deciding whether the conjunction of a finite set of Σ-literals is satisfiable in a model of T. 1All the signatures we consider are finite, and the equality symbol is considered as a logical symbol like boolean connectives and quantifiers.