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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 metadatas

https://hal.inria.fr/inria-00576594
Contributor : Christophe Ringeissen <>
Submitted on : Monday, March 14, 2011 - 5:27:27 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Links full text

Identifiers

Citation

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⟩

Share

Metrics

Record views

131