Valentin Montmirail

ECAI Conference 2020 Conference Paper

Consolidating Modal Knowledge Bases

• Zied Bouraoui
• Jean-Marie Lagniez
• Pierre Marquis
• Valentin Montmirail

This paper introduces a novel approach to the consolidation of knowledge bases represented as modal logic formulae. The objective is to turn the given knowledge base into another knowledge base such that the latter is consistent even when the former is not. Our approach follows a strategy that locally spots and iteratively consolidates inconsistent subformulae of the input knowledge base. Existing methods for consolidating a knowledge base typically consist in selecting some of its maximal consistent subbases. Such methods are suited to the case the input is a (conjunctively-interpreted) set of formulae. However, they are inadequate when the input consists of a single inconsistent modal formula since, in the modal case, a formula cannot always be turned into a conjunction of simpler formulae. Furthermore, such methods consolidate any base consisting of a single inconsistent formula into the empty base. Our approach does not suffer from such limitations and preserves more information in the general case. From a computational point of view, it ensures that the size of the consolidated base is bounded by the size of the input knowledge base. We present some empirical results demonstrating the practical feasibility of our approach.

KR Conference 2018 Short Paper

Space-Awareness in a SAT-Based Approach For PSPACE Modal Logics

• Jean Marie Lagniez
• Daniel Le Berre
• Tiago de Lima
• Valentin Montmirail

IJCAI Conference 2017 Conference Paper

A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem

• Jean-Marie Lagniez
• Daniel Le Berre
• Tiago de Lima
• Valentin Montmirail

Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking large systems. Since then, it has been applied to many different problems. It especially proved to be an highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both a CEGAR and a RECAR approach for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.

AAAI Conference 2017 Conference Paper

A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem

• Thomas Caridroit
• Jean-Marie Lagniez
• Daniel Le Berre
• Tiago de Lima
• Valentin Montmirail

We present a SAT-based approach for solving the modal logic S5-satisfiability problem. That problem being NP-complete, the translation into SAT is not a surprise. Our contribution is to greatly reduce the number of propositional variables and clauses required to encode the problem. We first present a syntactic property called diamond degree. We show that the size of an S5-model satisfying a formula φ can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5satisfiability of that formula. We also propose a lightweight caching system which allows us to further reduce the size of the propositional formula. We implemented a generic SATbased approach within the modal logic S5 solver S52SAT. It allowed us to compare experimentally our new upper-bound against previously known one, i. e. the number of modalities of φ and to evaluate the effect of our caching technique. We also compared our solver against existing modal logic S5 solvers. The proposed approach outperforms previous ones on the benchmarks used. These promising results open interesting research directions for the practical resolution of others modal logics (e. g. K, KT, S4)