A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications

Abstract : Effective quantifier elimination procedures for first-order theories provide a powerful tool for generically solving a wide range of problems based on logical specifications. In contrast to general first-order provers, quantifier elimination procedures are based on a fixed set of admissible logical symbolswith an implicitly fixed semantics. This admits the use of sub-algorithms from symbolic computation. We are going to focus on quantifier elimination for the reals and its applications giving examples from geometry, verification, and the life sciences. Beyond quantifier elimination we are going to discuss recent results with a subtropical procedure for an existential fragment of the reals. This incomplete decision procedure has been successfully applied to the analysis of reaction systems in chemistry and in the life sciences.
Type de document :
Article dans une revue
Mathematics in Computer Science, Springer, 2017, 11 (3-4), pp.483 - 502. 〈10.1007/s11786-017-0319-z〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01648690
Contributeur : Thomas Sturm <>
Soumis le : jeudi 30 novembre 2017 - 13:21:51
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : jeudi 1 mars 2018 - 12:31:00

Fichier

10.1007_s11786-017-0319-z.pdf
Accord explicite pour ce dépôt

Identifiants

Citation

Thomas Sturm. A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications. Mathematics in Computer Science, Springer, 2017, 11 (3-4), pp.483 - 502. 〈10.1007/s11786-017-0319-z〉. 〈hal-01648690〉

Partager

Métriques

Consultations de la notice

75

Téléchargements de fichiers

21