Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints

Abstract : The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment.
Type de document :
Communication dans un congrès
de Moura, Leonardo. CADE 2017 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, Lecture Notes in Computer Science, 10395, pp.202-219, 2017, CADE 2017: Automated Deduction – CADE 26. 〈10.1007/978-3-319-63046-5_13〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01657026
Contributeur : Stephan Merz <>
Soumis le : mercredi 6 décembre 2017 - 11:48:16
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13

Fichier

authorcopy.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Andreas Teucke, Christoph Weidenbach. Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. de Moura, Leonardo. CADE 2017 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, Lecture Notes in Computer Science, 10395, pp.202-219, 2017, CADE 2017: Automated Deduction – CADE 26. 〈10.1007/978-3-319-63046-5_13〉. 〈hal-01657026〉

Partager

Métriques

Consultations de la notice

156

Téléchargements de fichiers

16