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

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


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
Number of pages13
ISBN (Electronic)9783031157073
ISBN (Print)9783031157066
Publication statusPublished - 29 Aug 2022
Event16th International Conference on Logic Programming and Non-monotonic Reasoning - Genoa, Italy
Duration: 5 Sep 20229 Sep 2022
Conference number: 16

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13416 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference16th International Conference on Logic Programming and Non-monotonic Reasoning
Abbreviated titleLPNMR 2022
Internet address


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