Search

Co-localisées avec la Plate-Forme Intelligence Artificielle (PFIA 2019); National audience; Modeling intention is essential to explain decisions made by agents. In this work, we propose a model of intention in epistemic games, represented in dynamic epistemic logic. Given a property and a sequence of actions already performed by a player in such a game, we propose a method able to determine whether the player had the intention to obtain the property. An example of the method is given using a simplified version of the collaborative game Hanabi.; Modéliser l’intention permet d’expliquer les décisions prises par des agents. Dans ce travail, nous proposons une modélisation de l’intention dans des jeux épistémiques représentés en logique épistémique dynamique. Étant données une propriété et une suite d’actions déjà réalisée par un joueur dans un tel jeu, nous proposons une méthode capable de déterminer si le joueur a eu l’intention d’obtenir cette propriété. Un exemple de l’utilisation de cette méthode est donné en utilisant une version simplifiée du jeu collaboratif Hanabi.

International audience; Le solveur SAT est devenu un oracle NP e cace pour résoudre des problèmes NP-complet (voir au-delà). En gé-néral, ces problèmes sont résolus soit par une traduction di-recte vers SAT soit en résolvant itérativement des problèmes SAT dans une procédure comme CEGAR. Récemment, une nouvelle boucle CEGAR récursive travaillant sur deux ni-veaux d'abstractions, appelée RECAR, a été proposée et ins-tanciée pour la logique modale K. Nous visons à compléter ce travail pour les logiques modales utilisant les axiomes (B), (D), (T), (4) et (5). De plus, pour le rendre performant en pratique, nous généralisons le framework RECAR pour uti-liser des compositions de fonctions d'abstraction. Les résul-tats expérimentaux montrent l'e cacité de cette approche et qu'elle surpasse les solveurs de l'état de l'art pour les lo-giques modales K, KT et S4 sur les benchmarks considérés. Abstract SAT technology has become an e cient running NP-oracle for solving NP-complete problems (and beyond). Usually those problems are solved by direct translation to SAT or by solving iteratively SAT problems in a procedure like CEGAR. Recently, a new recursive CEGAR loop working with two abstraction levels, called RECAR, was proposed and instantiated for modal logic K. We aim to complete this work for modal logics based on axioms (B), (D), (T), (4) and (5). Moreover, to make it e cient in practice, we generalize the RECAR framework to deal with compositions of abstraction functions. Experimental results show that the approach is e cient and outperforms state-of-the-art modal logic solvers for modal logics K, KT and S4 on considered benchmarks.

National audience

National audience; Cet article présente une première étape vers une comparaison expérimentale rigoureuse de l'état de l'art pour la résolution pratique de la satisfiabilité de formules en logique modale K. Basé sur l'expérience acquise ces vingt dernières années sur l'évaluation de solveurs dans le cadre de la logique propositionnelle (SAT, MAXSAT, PBO, QBF), nous présentons un cadre pour comparer les performances de solveurs en logique modale K, permettant dans certains cas de valider les réponses des solveurs. Nous proposons pour cela un format de certificat et un vérificateur pour valider ces certificats. Nous présentons quelques résultats expérimentaux de solveurs de l'état de l'art, modifiés pour intégrer cette étape de vérification. Nous avons pu valider 67% des réponses SAT renvoyées par ces solveurs, ce qui permet d'obtenir un ensemble de problèmes avec une réponse validée indépendamment qui peut être réutilisée pour valider de nouveaux solveurs. Nous discutons la limite de notre approche dans la dernière partie de cet article.

International audience; Nous nous intéressons au problème de la gestion des incohérences dans des ontologies légères. Nous supposons que les bases de connaissances terminologiques (TBox) sont spécifiées dans les logiques de description DL-Lite. Nous supposons aussi que les bases assertionnelles (ABox) sont partiellement préordonnées et peuvent être incohérentes avec la base terminologique TBox. Une contribution im-portante de cet article est la proposition d'une méthode ef-ficace et saine, appelée Elect, pour restaurer la cohérence de la base ABox par rapport à la base TBox. Notre mé-thode permet de retrouver la sémantique dite IAR (Intersec-tion ABox Repair) lorsque la base ABox est non-ordonnée. Elle permet également de retrouver la sémantique dite non-contestée lorsque la base ABox est totalement préordonnée. La justification sémantique de la méthode Elect est basée d'abord sur le fait qu'une base ABox partiellement préor-donnée est interprétée comme une famille de bases ABox to-talement préordonnées. Ensuite, la méthode Elect applique l'inférence non-contestée à chacune de ces ABox totalement préordonnées. Dans la deuxième partie de l'article, nous in-troduisons le concept d'assertions, dites élues, qui permet de donner une caractérisation équivalente de la méthode Elect sans avoir à générer explicitement toutes les bases ABox to-talement préordonnées. Nous montrons alors que le calcul des assertions élues se fait en temps polynomial. Abstract We focus on the problem of handling inconsistency in lightweight ontologies. We assume that terminological knowledge bases (TBoxes) are specified in DL-Lite and that assertional facts (ABoxes) are partially preordered and may be inconsistent with respect to TBoxes. One of the main contributions of this paper is the provision of an efficient and safe method, called Elect, to restore consistency of the ABox with respect to the TBox. In the case where the ABox * Cet article est paru en anglais dans les actes de 15 th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Philadelphie, USA, 3-7 Juin 2019, pages 210-223, Springer. is flat (no priorities are associated with the assertions) or totally preordered, our method collapses with the well-known IAR semantics and non-defeated semantics, respectively. The semantic justification of Elect is obtained by first viewing a partially preordered ABox as a family of totally pre-ordered ABoxes, and then applying non-defeated inference to each of the totally preordered ABoxes. We introduce the concept of elected assertions which allows us to provide an equivalent characterisation of Elect without explicitly generating all totally preordered ABoxes. Finally we show that the computation of Elect is done in polynomial time.

International audience; Nous présentons une approche générale pour le raison-nement sur des séquences temporelles d'informations quali-tatives. Cette approche, qui s'appuie sur le cadre récemment introduit des multialgèbres, est de façon générale plus effi-cace computationnellement que les techniques de la littéra-ture. Nous appliquons notre approche au cas spécifique des séquences d'informations topologiques sur des régions de taille constante ; nous montrons que le formalisme obtenu dispose d'une procédure complète pour la décision de la co-hérence, et nous identifions ses trois sous-classes maximales contenant toutes les relations basiques. Abstract Relying on the recently introduced multi-algebras, we present a general approach for reasoning about temporal sequences of qualitative information that is generally compu-tationally more efficient than existing techniques. Applying our approach to the specific case of sequences of topolog-ical information about constant-size regions, we show that the resulting formalism has a complete procedure for deciding consistency, and we identify its three maximal tractable subclasses containing all basic relations.

International audience

We propose in this paper a modal logic to reason on the trust of an agent towards a statement formulated by another agent. Our model considers a doxastic trust modality inspired from the work of Dundua and Uridia. We combine this modality with a STIT formalism that allows us to express that an agent trust another one when this latter states it will sees to it that a statement is true. Furthermore we can express a dispositional trust like Herzig et al. and we show that our formalism allows to deduce some axioms given by Singh. Finally, we propose some ways to express collective trust., Nous proposons dans cet article une logique modale permettant de raisonner sur la confiance d'un agent en-vers le discours d'un autre agent. Notre modèle considère une modalité de confiance doxastique similaire à celle initialement introduite par Dundua et Uridia. En combinant cette formulation générale avec un formalisme STIT, nous exprimons aussi la confiance qu'un agent accorde a un autre lorsque ce dernier annonce qu'il veille à réaliser un énoncé. Nous retrouvons alors la notion de confiance dispositionnelle formalisée par Herzig et al. et caractérisons certaines propriétés qui avaient été axiomatisées par Singh. Enfin, nous montrons que notre modèle permet d'exprimer des notions de confiance collective.

International audience

International audience

International audience

National audience; L’extension des ensembles d’exemples est une questionimportante en apprentissage automatique. En effetquand les exemples disponibles sont en quantité limitée,les performances des méthodes classiques de classificationpeuvent diminuer, et il peut être désirable de construiredes exemples additionnels. Dans cet article, nous considéronsl’usage du raisonnement analogique, et plus particulièrement des proportions analogiques pour étendre les ensemblesd’exemples. On fait l’hypothèse que les classes sontdéterminées par une fonction (partiellement connue). Onexamine les conditions requises sur les fonctions pour garantirune extension sans erreur des ensembles d’exemples,dans un cadre booléen. Dans ce but, on introduit la notionde fonctions préservant l’analogie (fonctions PA), et nousétablissons qu’elles coïncident avec la classe des fonctionsbooléennes affines. Ce résultat théorique est complété parune étude expérimentale de PA-fonctions approchées, ce quisuggère qu’elles peuvent rester adéquates pour étendre desensembles d’exemples.