Goto

Collaborating Authors

 Logic & Formal Reasoning


JASP: A Framework for Integrating Answer Set Programming with Java

AAAI Conferences

Answer Set Programming (ASP) is a fully-declarative logic programming paradigm, which has been proposed in the area of knowledge representation and non-monotonic reasoning. Nowadays, the formal properties of ASP are well-understood, efficient ASP systems are available, and, recently, ASP has been employed in a few industrial applications. However, ASP technology is not mature for a successful exploitation in industry yet; mainly because ASP technologies are not integrated in the well-assessed development processes and platforms which are tailored for imperative/object-oriented programming languages. In this paper we present a new programming framework blending ASP with Java. The framework is based on JASP, an hybrid language that transparently supports a bilateral interaction between ASP and Java. JASP specifications are compliant with the JPA standard to perfectly fit extensively-adopted enterprise application technologies. The framework also encompasses an implementation of JASP as a plug-in for the Eclipse platform, called JDLV, which includes a compiler from JASP to Java. Moreover, we show a real-world application developed with JASP and JDLV, which highlights the effectiveness of our ASPโ€“Java integration framework.


Stable Models in Generalized Possibilistic Logic

AAAI Conferences

Possibilistic logic is a well-known logic for reasoning under uncertainty, which is based on the idea that the epistemic state of an agent can be modeled by assigning to each possible world a degree of possibility, taken from a totally ordered, but essentially qualitative scale. Recently, a generalization has been proposed that extends possibilistic logic to a meta-epistemic logic, endowing it with the capability of reasoning about epistemic states, rather than merely constraining them. In this paper, we further develop this generalized possibilistic logic (GPL). We introduce an axiomatization showing that GPL is a fragment of a graded version of the modal logic KD, and we prove soundness and completeness w.r.t. a semantics in terms of possibility distributions. Next, we reveal a close link between the well-known stable model semantics for logic programming and the notion of minimally specific models in GPL. More generally, we analyze the relationship between the equilibrium logic of Pearce and GPL, showing that GPL can essentially be seen as a generalization of equilibrium logic, although its notion of minimal specificity is slightly more demanding than the notion of minimality underlying equilibrium logic.


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.