Modal Logic S5 in Answer Set Programming with Lazy Creation of Worlds

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Modal logic S5 is used extensively for representing knowledge that includes statements about necessity and possibility, owing to its simplicity in handling chained modal operators. Significant research effort has been devoted in developing efficient reasoning mechanisms over complex S5 formulas, resulting in various solvers taking advantage of the boolean satisfiability problem (SAT). Among them, the most performant solver implements a heuristic for identifying worlds that can be merged, hence reducing the size of SAT instances to be checked. Recently, Answer Set Programming (ASP) has also been considered, and different ASP encodings were proposed and tested, reaching state-of-the-art performance. In particular, a heuristic for identifying the propositional atoms that are relevant in every world resulted in a performance gain in previous experiments. This work addresses the open question of whether the aforementioned two heuristics can be combined, as well as possibly enabling lazy instantiation of the resulting encodings, and what their potential impact is on the performance of the ASP-based solver. Experiments show that lazy creation of worlds provides some further performance gain to the ASP-based solver on the tested instances.
Original languageEnglish
Title of host publicationLogic Programming and Nonmonotonic Reasoning
Subtitle of host publication16th International Conference, LPNMR 2022, Genoa, Italy, September 5–8, 2022, Proceedings
EditorsGeorg Gottlob, Daniela Inclezan, Marco Maratea
Place of PublicationCham
PublisherSpringer, Cham
Volume13416
ISBN (Print)9783031157080
Publication statusAccepted/In press - 10 Jun 2022
Event16th International Conference on Logic Programming and Non-monotonic Reasoning - Genoa, Italy
Duration: 5 Sep 20228 Sep 2022
Conference number: 16
https://sites.google.com/view/lpnmr2022/home

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume13416
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International Conference on Logic Programming and Non-monotonic Reasoning
Abbreviated titleLPNMR 2022
Country/TerritoryItaly
CityGenoa
Period5/09/228/09/22
Internet address

Fingerprint

Dive into the research topics of 'Modal Logic S5 in Answer Set Programming with Lazy Creation of Worlds'. Together they form a unique fingerprint.

Cite this