In abstract algebra, a structure is said to be Noetherian if it does not admit infinite strictly ascending chains of congruences. In this paper, we adapt this notion to first-order logic by defining the class of Noetherian theories. Examples of theories in this class are Linear Arithmetics without ordering and the empty theory containing only a unary function symbol. Interestingly, it is possible to design a non-disjoint combination method for extensions of Noetherian theories. We investigate sufficient conditions for adding a temporal dimension to such theories in such a way that the decidability of the satisfiability problem for the quantifier-free fragment of the resulting temporal logic is guaranteed. This problem is firstly investigated for the case of Linear time Temporal Logic and then generalized to arbitrary modal/temporal logics whose propositional relativized satisfiability problem is decidable. © Springer-Verlag Berlin Heidelberg 2007.
Noetherianity and combination problems / Ghilardi, S.; Nicolini, E.; Ranise, S.; Zucchelli, D.. - 4720:(2007), pp. 206-220. (Intervento presentato al convegno 6th International Symposium on Frontiers of Combining Systems, FroCoS 2007 tenutosi a Liverpool, gbr nel 2007) [10.1007/978-3-540-74621-8_14].
Noetherianity and combination problems
Ranise S.;
2007-01-01
Abstract
In abstract algebra, a structure is said to be Noetherian if it does not admit infinite strictly ascending chains of congruences. In this paper, we adapt this notion to first-order logic by defining the class of Noetherian theories. Examples of theories in this class are Linear Arithmetics without ordering and the empty theory containing only a unary function symbol. Interestingly, it is possible to design a non-disjoint combination method for extensions of Noetherian theories. We investigate sufficient conditions for adding a temporal dimension to such theories in such a way that the decidability of the satisfiability problem for the quantifier-free fragment of the resulting temporal logic is guaranteed. This problem is firstly investigated for the case of Linear time Temporal Logic and then generalized to arbitrary modal/temporal logics whose propositional relativized satisfiability problem is decidable. © Springer-Verlag Berlin Heidelberg 2007.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
