Delmas, Rémi and Garion, Christophe
and Giet, Josselin
MOLOSS, un solveur pour la satisfiabilité en logique modale.
(2018)
In: Journées de l'Intelligence Artificielle Fondamentale (JIAF-2018), 13 June 2018 - 15 June 2018 (Amiens, France).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 498kB |
Official URL: https://home.mis.u-picardie.fr/~evenement/JIAF2018/articles/JIAF_2018_papier_12.pdf
Abstract
Cet article présente MOLOSS, un solveur pour la satisfiabilité en logique modale. MOLOSS implémente et étend le travail théorique d'Aceres et al. dans lequel les auteurs définissent une procédure de décision basée SMT pour les logiques modales. Cette procédure traduit classiquement une formule de la logique modale en une formule du premier ordre et instancie les quantificateurs de la formule résultante pour vérifier sa satifaisabilité en utilisant un solveur SAT. Notre implémantation permet de comparer la procédure d'Aceres et al. avec une autre dans laquelle les quantificateurs de la formule du premier ordre sont gérés directement par le solveur SMT utilisé.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Audience (conference): | National conference proceedings |
| Uncontrolled Keywords: | |
| Institution: | Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE) French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE) Other partners > Ecole Normale Supérieure de Paris - ENS Paris (FRANCE) |
| Laboratory name: | |
| Statistics: | download |
| Deposited By: | Christophe Garion |
| Deposited On: | 21 Jun 2018 08:52 |
Repository Staff Only: item control page
