English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In the last two decades, modal and description logics have been applied tonumerous areas of computer science, including knowledge representation, formalverification, database theory, distributed computing and, more recently,semantic web and ontologies. For this reason, the problem of automatedreasoning in modal and description logics has been thoroughly investigated. Inparticular, many approaches have been proposed for efficiently handling thesatisfiability of the core normal modal logic K(m), and of its notationalvariant, the description logic ALC. Although simple in structure, K(m)/ALC iscomputationally very hard to reason on, its satisfiability beingPSPACE-complete.  In this paper we start exploring the idea of performing automated reasoningtasks in modal and description logics by encoding them into SAT, so that to behandled by state-of-the-art SAT tools; as with most previous approaches, webegin our investigation from the satisfiability in K(m). We propose anefficient encoding, and we test it on an extensive set of benchmarks, comparingthe approach with the main state-of-the-art tools available. Although theencoding is necessarily worst-case exponential, from our experiments we noticethat, in practice, this approach can handle most or all the problems which areat the reach of the other approaches, with performances which are comparablewith, or even better than, those of the current state-of-the-art tools.

Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability