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.
|Titolo:||Noetherianity and Combination Problems|
|Settore Scientifico Disciplinare:||Settore M-FIL/02 - Logica e Filosofia della Scienza|
|Data di pubblicazione:||2007|
|Digital Object Identifier (DOI):||10.1007/978-3-540-74621-8_14|
|Tipologia:||Book Part (author)|
|Appare nelle tipologie:||03 - Contributo in volume|