OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

MOLOSS, un solveur pour la satisfiabilité en logique modale

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).

[img]
Preview
(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