Noetherianity and Combination Problems

10 years 2 months ago
Noetherianity and Combination Problems
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.
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, D
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Authors Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
Comments (0)