Goto

Collaborating Authors

 Logic & Formal Reasoning


From Knowledge Represented in Frame-Based Languages to Declarative Representation and Reasoning via ASP

AAAI Conferences

In this paper we encode some of the reasoning methods used in frame based knowledge representation languages in answer set programming (ASP). In particular, we show how ``cloning'' and ``unification'' in frame based systems can be encoded in ASP. We then show how some of the types of queries with respect to a biological knowledge base can be encoded using our methodology. We also provide insight on how the reasoning can be done more efficiently when dealing with a huge knowledge base.


Paraconsistent Hybrid Theories

AAAI Conferences

We consider the problem of reasoning from inconsistent hybrid theories, i.e., combinations of a structural part given by a classical first order theory (e.g., an ontology) and a rules part as a set of declarative logic program rules (under answer-set semantics). Paraconsistent reasoning is achieved by defining an appropriate semantics, so-called paraconsistent semi-equilibrium model semantics for such hybrid theories. Appropriateness of the semantics is established with respect to desirable properties attesting design objectives, such us to generalize the underlying semantics in case of consistency, as well as to generalize existing paraconsistent semantics for the individual parts. A complexity analysis of corresponding reasoning tasks complements these results.


Declarative Entity Resolution via Matching Dependencies and Answer Set Programs

AAAI Conferences

Entity resolution (ER) is an important and common problem in data cleaning. It is about identifying and merging records in a database that represent the same real-world entity. Recently, matching dependencies (MDs) have been introduced and investigated as declarative rules that specify ER. An ER process induced by MDs over a dirty instance leads to multiple clean instances, in general. In this work, we present disjunctive answer set programs (with stable model semantics) that capture through their models the class of alternative clean instances obtained after an ER process based on MDs. With these programs, we can obtain clean answers to queries, i.e. those that are invariant under the clean instances, by skeptically reasoning from the program. We investigate the ER programs in terms of expressive power for the ER task at hand. As an important special and practical case of ER, we provide a declarative reconstruction of the so-called union-case ER methodology, as presented through a generic approach to ER (the so-called Swoosh approach).


Ordered Epistemic Logic: Semantics, Complexity and Applications

AAAI Conferences

Many examples of epistemic reasoning in the literature exhibit a stratified structure: defaults are formulated on top of an incomplete knowledge base. These defaults derive extra information in case information is missing in the knowledge base. In autoepistemic logic, default logic and ASP this inherent stratification is not preserved as they may refer to their own knowledge or logical consequences. Defining the semantics of such logics requires a complex mathematical construction. As an alternative, this paper further develops ordered epistemic logic. This logic extends first order logic with a modal operator and stratification is maintained. This allows us to define an easy to understand semantics. Moreover, inference tasks have a lower complexity than in autoepistemic logic and the logic integrates seamlessly into classical logic and its extensions. In this paper we also propose a generalization of ordered epistemic logic, which we call distributed ordered epistemic logic. We argue that it can provide a semantic foundation for a number of distributed knowledge representation formalisms found in the literature.


Abstract Normative Systems: Semantics and Proof Theory

AAAI Conferences

In this paper we introduce an abstract theory of normative reasoning, whose central notion is the generation of obligations, permissions and institutional facts from conditional norms. We present various semantics and their proof systems. The theory can be used to classify and compare new candidates for standards of normative reasoning, and to explore more elaborate forms of normative reasoning than studied thus far.


Only-Knowing Meets Nonmonotonic Modal Logic

AAAI Conferences

Only-knowing was originally introduced by Levesque to capture the beliefs of an agent in the sense that its knowledge base is all the agent knows. When a knowledge base contains defaults Levesque also showed an exact correspondence between only-knowing and autoepistemic logic. Later these results were extended by Lakemeyer and Levesque to also capture a variant of autoepistemic logic proposed by Konolige and Reiter's default logic. One of the benefits of such an approach is that various nonmonotonic formalisms can be compared within a single monotonic logic leading, among other things, to the first axiom system for default logic. In this paper, we will bring another large class of nonmonotonic systems, which were first studied by McDermott and Doyle, into the only-knowing fold. Among other things, we will provide the first possible-world semantics for such systems, providing a new perspective on the nature of modal approaches to nonmonotonic reasoning.


Automated Verification of Epistemic Properties for General Game Playing

AAAI Conferences

Automatically deriving properties of new games is one of the fundamental challenges for general game-playing systems, whose task is to learn to play any previously unknown game solely by being given the rules of that game. A recently developed method uses Answer Set Programming for verifying finitely-bounded temporal invariance properties against a given game description by structural induction. Addressing the new challenge posed by the recent extension of the general Game Description Language to include games with imperfect information and randomness, we extend this method to epistemic properties about games. We formally prove this extension to be correct, and we report on experiments that show its practical applicability.


An Abstraction Technique for the Verification of Artifact-Centric Systems

AAAI Conferences

We explore the paradigm of artifact-centric systems from a knowledge-based perspective. We provide a semantics based on interpreted-systems to interpret a first-order temporal- epistemic language with identity in a multi-agent setting. We consider the model checking problem for this language and provide abstraction results. We isolate a natural subclass of artifact-systems for which the model checking problem is decidable. We give an upper bound on the complexity of the model checking problem.


Rewriting Ontological Queries into Small Nonrecursive Datalog Programs

AAAI Conferences

We consider the setting of ontological database access, where an A-box is given in form of a relational database D and where a Boolean conjunctive query q has to be evaluated against D modulo a T-box Σ formulated in DL-Lite or Linear Datalog+/-. It is well-known that (Σ, q) can be rewritten into an equivalent nonrecursive Datalog program P that can be directly evaluated over D. However, for Linear Datalog+/- or for DL-Lite versions that allow for role inclusion, the rewriting methods described so far result in a nonrecursive Datalog program P of size exponential in the joint size of Σ and q . This gives rise to the interesting question whether such a rewriting necessarily needs to be of exponential size. In this paper we show that it is actually possible to translate (Σ, q ) into a polynomially sized equivalent nonrecursive Datalog program P.


Strong Equivalence of Qualitative Optimization Problems

AAAI Conferences

We introduce the framework of qualitative optimization problems (or, simply, optimization problems) to represent preference theories. The formalism uses separate modules to describe the space of outcomes to be compared (the generator) and the preferences on outcomes (the selector). We consider two types of optimization problems. They differ in the way the generator, which we model by a propositional theory, is interpreted: by the standard propositional logic semantics, and by the equilibrium-model (answer-set) semantics. Under the latter interpretation of generators, optimization problems directly generalize answer-set optimization programs proposed previously. We study strong equivalence of optimization problems, which guarantees their interchangeability within any larger context. We characterize several versions of strong equivalence obtained by restricting the class of optimization problems that can be used as extensions and establish the complexity of associated reasoning tasks. Understanding strong equivalence is essential for modular representation of optimization problems and rewriting techniques to simplify them without changing their inherent properties.