Chapter 32. SAT Techniques for Modal and Description Logics

2021 ◽  
Author(s):  
Roberto Sebastiani ◽  
Armando Tacchella
Keyword(s):  
Computer Science ◽  
Automated Reasoning ◽  
Description Logics ◽  
Theoretical Framework ◽  
Modal Logics

In the last two decades, modal and description logics have provided a theoretical framework for important applications in many areas of computer science. For this reason, the problem of automated reasoning in modal and description logics has been thoroughly investigated. In this chapter we show how efficient Boolean reasoning techniques have been imported, used and integrated into reasoning tools for modal and description logics. To this extent, we focus on modal logics, and in particular mainly on K(m). In particular, we provide some background in modal logics; we describe a basic theoretical framework and we present and analyze the basic tableau-based and DPLL-based techniques; we describe optimizations and extensions of the DPLL-based procedures; we introduce the automata-theoretic/OBDD-based approach; finally, we present the eager approach.

scholarly journals Fusions of Description Logics and Abstract Description Systems

2002 ◽  
Vol 16 ◽  
pp. 1-58 ◽  
Author(s):  
F. Baader ◽  
C. Lutz ◽  
H. Sturm ◽  
F. Wolter
Keyword(s):  
Large Class ◽  
Description Logics ◽  
General Setting ◽  
Modal Logics ◽  
Common Generalization ◽  
Abstract Description ◽  
Normal Modal Logics ◽  
Combining Logics

Fusions are a simple way of combining logics. For normal modal logics, fusions have been investigated in detail. In particular, it is known that, under certain conditions, decidability transfers from the component logics to their fusion. Though description logics are closely related to modal logics, they are not necessarily normal. In addition, ABox reasoning in description logics is not covered by the results from modal logics. In this paper, we extend the decidability transfer results from normal modal logics to a large class of description logics. To cover different description logics in a uniform way, we introduce abstract description systems, which can be seen as a common generalization of description and modal logics, and show the transfer results in this general setting.

scholarly journals KRIPKE COMPLETENESS OF STRICTLY POSITIVE MODAL LOGICS OVER MEET-SEMILATTICES WITH OPERATORS

2019 ◽  
Vol 84 (02) ◽  
pp. 533-588 ◽  
Author(s):  
STANISLAV KIKOT ◽  
AGI KURUCZ ◽  
YOSHIHITO TANAKA ◽  
FRANK WOLTER ◽  
MICHAEL ZAKHARYASCHEV
Keyword(s):  
Computer Science ◽  
Monotone Operators ◽  
Modal Logics ◽  
Consequence Relations ◽  
First Order ◽  
Completeness Problem ◽  
Relational Structures ◽  
Kripke Frames

AbstractOur concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given spi-logic.

THE MULTIAGENT TECHNOLOGY AND PARADIGM WITHIN SCIENTIFIC DISCOVERY

2007 ◽  
Vol 16 (02) ◽  
pp. 219-242 ◽  
Author(s):  
FRANCESCO AMIGONI ◽  
VIOLA SCHIAFFONATI
Keyword(s):  
Computer Science ◽  
Philosophy Of Science ◽  
Multiagent Systems ◽  
Scientific Practice ◽  
Scientific Discovery ◽  
Theoretical Framework ◽  
The Other ◽  
Research Activity ◽  
Scientific Results ◽  
The One

Scientific practice has been rapidly evolving in the last years under the pressure of developments in computer science and technology. In this paper we present some of the results of our research activity at the boundary between computer science and philosophy of science started in 1997 under Marco Somalvico's impulse and guidance. In particular, we discuss two roles that multiagent systems can play in scientific discovery. From the one hand, they can support scientific practice; from the other hand, they can represent scientific results. The theoretical framework presented in this paper is exemplified in concrete by illustrating specific implemented systems, both taken from the literature and developed by ourselves.

Reconsidering Conventional Markup for Knowledge Representation

2009 ◽  
Author(s):  
David Dubin ◽  
David J. Birnbaum
Keyword(s):  
Semantic Web ◽  
Automated Reasoning ◽  
Description Logics ◽  
Manuscript Studies ◽  
Semantic Web Technologies ◽  
Web Technologies ◽  
Programming Tools ◽  
Textual Transmission ◽  
Main Attraction

The main attraction of semantic web technologies such as RDF and OWL over conventional markup is the support those tools provide for expressing precise semantics. Formal grounding for RDF-based languages (in, for example, description logics) and their integration with logic programming tools are guided and constrained by issues of decidability and the tractability of computations. Users of these technologies are invited to use less expressive representations, and thereby work within those constraints. Such compromises seem reasonable when considering the roles automated reasoning agents are expected to play by the semantic web community. But where expectations differ, it may be useful to reconsider using conventional markup and inferencing methods that have been applied with success despite their theoretical weaknesses. We illustrate these issues with a case study from manuscript studies and textual transmission.

The Role of Foundational Ontologies for Domain Ontology Engineering

2010 ◽  
Vol 1 (2) ◽  
pp. 1-22 ◽  
Author(s):  
Giancarlo Guizzardi ◽  
Fernanda Baião ◽  
Mauro Lopes ◽  
Ricardo Falbo
Keyword(s):  
Computer Science ◽  
Automated Reasoning ◽  
Oil And Gas ◽  
Reference Model ◽  
Ontology Engineering ◽  
Modeling Language ◽  
Engineering Process ◽  
Industrial Case Study

Ontologies are commonly used in computer science either as a reference model to support semantic interoperability, or as an artifact that should be efficiently represented to support tractable automated reasoning. This duality poses a tradeoff between expressivity and computational tractability that should be addressed in different phases of an ontology engineering process. The inadequate choice of a modeling language, disregarding the goal of each ontology engineering phase, can lead to serious problems in the deployment of the resulting model. This article discusses these issues by making use of an industrial case study in the domain of Oil and Gas. The authors make the differences between two different representations in this domain explicit, and highlight a number of concepts and ideas that were implicit in an original OWL-DL model and that became explicit by applying the methodological directives underlying an ontologically well-founded modeling language.

Semantics for the Semantic Web

2011 ◽  
pp. 1-21 ◽  
Author(s):  
Amit Sheth ◽  
Cartic Ramakrishnan ◽  
Christopher Thomas
Keyword(s):  
Semantic Web ◽  
Computer Science ◽  
Description Logics ◽  
Heterogeneous Data ◽  
Research Areas ◽  
Broad Variety ◽  
Semantic Techniques

Enabling applications that exploit heterogeneous data in the Semantic Web will require us to harness a broad variety of semantics. Considering the role of semantics in a number of research areas in computer science, we organize semantics in three forms — implicit, formal, and powerful — and explore their roles in enabling some of the key capabilities related to the Semantic Web. The central message of this article is that building the Semantic Web purely on description logics will artificially limit its potential, and that we will need to both exploit well-known techniques that support implicit semantics, and develop more powerful semantic techniques.

Sign in / Sign up

Export Citation Format

Share Document