Skip to Main content Skip to Navigation
New interface
Conference papers

Noetherianity and Combination Problems

Silvio Ghilardi 1 Enrica Nicolini 2 Silvio Ranise 2 Daniele Zucchelli 1, 2 
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Monday, March 14, 2011 - 5:27:27 PM
Last modification on : Tuesday, November 22, 2022 - 5:32:24 PM

Links full text



Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli. Noetherianity and Combination Problems. Frontiers of Combining Systems, Sep 2007, Liverpool, United Kingdom. pp.206-220, ⟨10.1007/978-3-540-74621-8_14⟩. ⟨inria-00576594⟩



Record views