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.
Type de document :
Communication dans un congrès
Boris Konev and Frank Wolter. Frontiers of Combining Systems, Sep 2007, Liverpool, United Kingdom. Springer, 4720, pp.206-220, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74621-8_14〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00576594
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 14 mars 2011 - 17:27:27
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral

Identifiants

Citation

Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli. Noetherianity and Combination Problems. Boris Konev and Frank Wolter. Frontiers of Combining Systems, Sep 2007, Liverpool, United Kingdom. Springer, 4720, pp.206-220, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74621-8_14〉. 〈inria-00576594〉

Partager

Métriques

Consultations de la notice

98