scholarly journals Prime Implicates and Prime Implicants: From Propositional to Modal Logic

2009 ◽  
Vol 36 ◽  
pp. 71-128 ◽  
Author(s):  
M. Bienvenu
Keyword(s):  
Artificial Intelligence ◽  
Modal Logic ◽  
Propositional Logic ◽  
Description Logic ◽  
Recognition Task ◽  
Abductive Reasoning ◽  
Upper And Lower Bounds ◽  
Knowledge Compilation ◽  
Prime Implicants ◽  
Computational Properties

Prime implicates and prime implicants have proven relevant to a number of areas of artificial intelligence, most notably abductive reasoning and knowledge compilation. The purpose of this paper is to examine how these notions might be appropriately extended from propositional logic to the modal logic K. We begin the paper by considering a number of potential definitions of clauses and terms for K. The different definitions are evaluated with respect to a set of syntactic, semantic, and complexity-theoretic properties characteristic of the propositional definition. We then compare the definitions with respect to the properties of the notions of prime implicates and prime implicants that they induce. While there is no definition that perfectly generalizes the propositional notions, we show that there does exist one definition which satisfies many of the desirable properties of the propositional case. In the second half of the paper, we consider the computational properties of the selected definition. To this end, we provide sound and complete algorithms for generating and recognizing prime implicates, and we show the prime implicate recognition task to be PSPACE-complete. We also prove upper and lower bounds on the size and number of prime implicates. While the paper focuses on the logic K, all of our results hold equally well for multi-modal K and for concept expressions in the description logic ALC.

Knowledge-Based Description Logic ALCO Knowledge Compiled Algorithm to Determine Consistency

2012 ◽  
Vol 487 ◽  
pp. 347-351
Author(s):  
Ya Qiong Jiang ◽  
Jun Wang
Keyword(s):  
Normal Form ◽  
Knowledge Base ◽  
Propositional Logic ◽  
Description Logic ◽  
Knowledge Bases ◽  
Knowledge Compilation ◽  
Knowledge Based ◽  
Common Technique ◽  
Compilation Techniques

Knowledge compilation is a common technique for propositional logic knowledge bases. A given knowledge base is transformed into a normal form, for which reasoning can be answered efficiently. The precompilation of description logic knowledge base is important for reasoning and services of description logic. This paper gives precompilation about the description logic ALCO TBox based on knowledge compilation techniques, for which the consistency of TBox can be determined.

Boolean Role Inclusions in DL-Lite With and Without Time

2020 ◽  
Author(s):  
Roman Kontchakov ◽  
Vladislav Ryzhikov ◽  
Frank Wolter ◽  
Michael Zakharyaschev
Keyword(s):  
Description Logic ◽  
Expressive Power ◽  
Necessary Condition ◽  
Data Complexity ◽  
Temporal Dimension ◽  
Complexity Level ◽  
Primitive Recursion ◽  
Lower Complexity ◽  
Computational Properties

Traditionally, description logic has focused on representing and reasoning about classes rather than relations (roles), which has been justified by the deterioration of the computational properties if expressive role inclusions are added. The situation is even worse in the temporalised setting, where monodicity is viewed as an almost necessary condition for decidability. We take a fresh look at the description logic DL-Lite with expressive role inclusions, both with and without a temporal dimension. While we confirm that full Boolean expressive power on roles leads to FO^2-like behaviour in the atemporal case and undecidability in the temporal case, we show that, rather surprisingly, the restriction to Krom and Horn role inclusions leads to much lower complexity in the atemporal case and to decidability (and ExpSpace-completeness) in the temporal case, even if one admits full Booleans on concepts. The latter result is one of very few instances breaking the monodicity barrier in temporal FO. This is also reflected on the data complexity level, where we obtain new rewritability results into FO with relational primitive recursion and FO with unary divisibility predicates.

On the Decidability of Expressive Description Logics with Transitive Closure and Regular Role Expressions

2020 ◽  
Author(s):  
Jean Christoph Jung ◽  
Carsten Lutz ◽  
Thomas Zeume
Keyword(s):  
Modal Logic ◽  
Description Logic ◽  
Transitive Closure ◽  
Description Logics ◽  
Regular Expressions ◽  
Linear Orders ◽  
Functional Roles

We consider fragments of the description logic SHOIF extended with regular expressions on roles. Our main result is that satisfiability and finite satisfiability are decidable in two fragments SHOIF^1 and SHOIF^2, NExpTime-complete for the former and in 2NExpTime for the more expressive latter fragment. Both fragments impose restrictions on regular role expressions of the form r*. SHOIF^1 encompasses the extension of SHOIF with transitive closure of roles (when functional roles have no subroles) and the modal logic of linear orders and successor, with converse. Consequently, these logics are also decidable and NExpTime-complete.

scholarly journals A PURELY SYNTACTIC AND CUT-FREE SEQUENT CALCULUS FOR THE MODAL LOGIC OF PROVABILITY

2009 ◽  
Vol 2 (4) ◽  
pp. 593-611 ◽  
Author(s):  
FRANCESCA POGGIOLESI
Keyword(s):  
Modal Logic ◽  
Propositional Logic ◽  
Sequent Calculus ◽  
Semantic Element ◽  
Modal Propositional Logic

In this paper we present a sequent calculus for the modal propositional logic GL (the logic of provability) obtained by means of the tree-hypersequent method, a method in which the metalinguistic strength of hypersequents is improved, so that we can simulate trees shapes. We prove that this sequent calculus is sound and complete with respect to the Hilbert-style system GL, that it is contraction free and cut free and that its logical and modal rules are invertible. No explicit semantic element is used in the sequent calculus and all the results are proved in a purely syntactic way.

KNOWLEDGE BASE REFORMATION: PREPARING FIRST-ORDER THEORIES FOR EFFICIENT PROPOSITIONAL REASONING

2000 ◽  
Vol 14 (01) ◽  
pp. 35-57 ◽  
Author(s):  
HELMUT PRENDINGER ◽  
MITSURU ISHIZUKA ◽  
GERHARD SCHURZ
Keyword(s):  
Knowledge Base ◽  
Propositional Logic ◽  
Knowledge Compilation ◽  
First Order ◽  
Order Language

We present an approach to knowledge compilation that transforms a function-free first-order Horn knowledge base to propositional logic. This form of compilation is important since the most efficient reasoning methods are defined for propositional logic, while knowledge is most conveniently expressed within a first-order language. To obtain compact propositional representations, we employ techniques from (ir)relevance reasoning as well as theory transformation via unfold/fold transformations. Application areas include diagnosis, planning, and vision. Preliminary experiments with a hypothetical reasoner indicate that our method may yield significant speed-ups.

scholarly journals Towards Trustable Explainable AI

2020 ◽  
Author(s):  
Alexey Ignatiev
Keyword(s):  
Artificial Intelligence ◽  
Machine Learning ◽  
Recent Work ◽  
Abductive Reasoning ◽  
Rigorous Approach ◽  
Explainable Artificial Intelligence ◽  
Explainable Ai ◽  
Close Relationship

Explainable artificial intelligence (XAI) represents arguably one of the most crucial challenges being faced by the area of AI these days. Although the majority of approaches to XAI are of heuristic nature, recent work proposed the use of abductive reasoning to computing provably correct explanations for machine learning (ML) predictions. The proposed rigorous approach was shown to be useful not only for computing trustable explanations but also for validating explanations computed heuristically. It was also applied to uncover a close relationship between XAI and verification of ML models. This paper overviews the advances of the rigorous logic-based approach to XAI and argues that it is indispensable if trustable XAI is of concern.

scholarly journals Razonamiento explicativo y evolución de lógicas: Una aproximación desde la semántica de mundos posibles

2012 ◽  
Vol 18 (2) ◽  
Author(s):  
Fernando Soler Toscano
Keyword(s):  
Modal Logic ◽  
Scientific Explanation ◽  
Abductive Reasoning ◽  
Kripke Frames

RESUMENRealizamos un acercamiento al razonamiento explicativo mediante estructuras modales. Usamos el formalismo bien conocido de los marcos de Kripke, pero asociamos a cada mundo, no una interpretación, sino una lógica. De este modo, definimos operadores que nos permiten expresar distintas modificaciones que puede sufrir una teoría, concretamente ampliaciones y contracciones. Mostramos cómo los tratamientos lógicos tradicionales del razonamiento abductivo pueden ser comprendidos desde nuestra propuesta.PALABRAS CLAVERAZONAMIENTO ABDUCTIVO, LÓGICAS NO CLÁSICAS, LÓGICA MODAL, MODELOS DE KRIPKE, EXPLICACIÓN CIENTÍFICA.ABSTRACTWe propose an approach to explanatory reasoning through modal structures. We use the wellknown formalism of Kripke frames, but associated with each world, there is not an interpretation but a logic. Then, we define operators that allow us to express different modifications of a theory, specially expansions and contractions. We show that traditional logical treatments of abductive reasoning can be understood from our proposal.KEYWORDSABDUCTIVE REASONING, NON-CLASSICAL LOGICS, MODAL LOGIC, KRIPKE FRAMES, SCIENTIFIC EXPLANATION.

scholarly journals A Resolution Method for Modal Logic S5

10.29007/1zgr ◽  
2018 ◽  
Author(s):  
Yakoub Salhi ◽  
Michael Sioutis
Keyword(s):  
Normal Form ◽  
Modal Logic ◽  
Graph Coloring ◽  
Propositional Logic ◽  
Possible Worlds ◽  
Conjunctive Normal Form ◽  
Clause Structure ◽  
Possible Worlds Semantics ◽  
Resolution Method ◽  
Resolution Rule

The aim of this work is to define a resolution method for the modal logic S5. Wefirst propose a conjunctive normal form (S5-CNF) which is mainly based on using labelsreferring to semantic worlds. In a sense, S5-CNF can be seen as a generalization of theconjunctive normal form in propositional logic by using in the clause structure the modalconnective of necessity and labels. We show that every S5 formula can be transformedinto an S5-CNF formula using a linear encoding. Then, in order to show the suitabilityof our normal form, we describe a modeling of the problem of graph coloring. Finally, weintroduce a simple resolution method for S5, composed of three deductive rules, and weshow that it is sound and complete. Our deductive rules can be seen as adaptations ofRobinson’s resolution rule to the possible-worlds semantics.

scholarly journals ABox Abduction via Forgetting in ALC

2019 ◽  
Vol 33 ◽  
pp. 2768-2775 ◽  
Author(s):  
Warren Del-Pinto ◽  
Renate A. Schmidt
Keyword(s):  
Prior Knowledge ◽  
Real World ◽  
Description Logic ◽  
Abductive Reasoning ◽  
The Other ◽  
Prototype Implementation ◽  
Redundancy Elimination ◽  
Horn Clauses ◽  
Hypothesis Space ◽  
Uniform Interpolation

Abductive reasoning generates explanatory hypotheses for new observations using prior knowledge. This paper investigates the use of forgetting, also known as uniform interpolation, to perform ABox abduction in description logic (ALC) ontologies. Non-abducibles are specified by a forgetting signature which can contain concept, but not role, symbols. The resulting hypotheses are semantically minimal and consist of a disjunction of ABox axioms. These disjuncts are each independent explanations, and are not redundant with respect to the background ontology or the other disjuncts, representing a form of hypothesis space. The observations and hypotheses handled by the method can contain both atomic or complex ALC concepts, excluding role assertions, and are not restricted to Horn clauses. Two approaches to redundancy elimination are explored in practice: full and approximate. Using a prototype implementation, experiments were performed over a corpus of real world ontologies to investigate the practicality of both approaches across several settings.

Sign in / Sign up

Export Citation Format

Share Document