Goto

Collaborating Authors

 Logic & Formal Reasoning


Modular Systems with Preferences

AAAI Conferences

We propose a versatile framework for combining knowledge bases in modular systems with preferences. In our formalism, each module (knowledge base) can be specified in a different language. We define the notion of a preference-based modular system that includes a formalization of meta-preferences. We prove that our formalism is robust in the sense that the operations for combining modules preserve the notion of  a preference-based modular system. Finally, we formally demonstrate correspondences between our framework and the related preference formalisms of cp-nets and preference-based planning. Our framework allows one to use  these preference formalisms (and others) in combination, in the same modular system.


The Cube of Opposition: A Structure Underlying Many Knowledge Representation Formalisms

AAAI Conferences

The square of opposition is a structure involving two involutive negations and relating quantified statements, invented in Aristotle time. Rediscovered in the second half of the XXth century, and advocated as being of interest for understanding conceptual structures and solving problems in paraconsistent logics, the square of opposition has been recently completed into a cube, which corresponds to the introduction of a third negation. Such a cube can be encountered in very different knowledge representation formalisms, such as modal logic, possibility theory in its all-or-nothing version, formal concept analysis, rough set theory and abstract argumentation. After restating these results in a unified perspective, the paper proposes a graded extension of the cube and shows that several qualitative, as well as quantitative formalisms, such as Sugeno integrals used in multiple criteria aggregation and qualitative decision theory, or yet belief functions and Choquet integrals, are amenable to transformations that form graded cubes of opposition. This discovery leads to a new perspective on many knowledge representation formalisms, laying bare their underlying common features. The cube of opposition exhibits fruitful parallelisms between different formalisms, which leads to highlight some missing components present in one formalism and currently absent from another.


Verification of Generalized Inconsistency-Aware Knowledge and Action Bases

AAAI Conferences

Knowledge and Action Bases (KABs) have been put forward as a semantically rich representation of a domain, using a DL KB to account for its static aspects, and actions to evolve its extensional part over time, possibly introducing new objects. Recently, KABs have been extended to manage inconsistency, with ad-hoc verification techniques geared towards specific semantics. This work provides a twofold contribution along this line of research. On the one hand, we enrich KABs with a high-level, compact action language inspired by Golog, obtaining so called Golog-KABs (GKABs). On the other hand, we introduce a parametric execution semantics for GKABs, so as to elegantly accomodate a plethora of inconsistency-aware semantics based on the notion of repair. We then provide several reductions for the verification of sophisticated first-order temporal properties over inconsistency-aware GKABs, and show that it can be addressed using known techniques, developed for standard KABs.


On the Undecidability of the Situation Calculus Extended with Description Logic Ontologies

AAAI Conferences

In this paper we investigate situation calculus action theories extended with ontologies, expressed as description logics TBoxes that act as state constraints. We show that this combination, while natural and desirable, is particularly problematic: it leads to undecidability of the simplest form of reasoning, namely satisfiability, even for the simplest kinds of description logics and the simplest kind of situation calculus action theories.


Logic Program Termination Analysis Using Atom Sizes

AAAI Conferences

Recent years have witnessed a great deal of interest in extending answer set programming with function symbols. Since the evaluation of a program with function symbols might not terminate and checking termination is undecidable, several classes of logic programs have been proposed where the use of function symbols is limited but the program evaluation is guaranteed to terminate. In this paper, we propose a novel class of logic programs whose evaluation always terminates. The proposed technique identifies terminating programs that are not captured by any of the current approaches. Our technique is based on the idea of measuring the size of terms and atoms to check whether the rule head size is bounded by the body, and performs a more fine-grained analysis than previous work. Rather than adopting an all-or-nothing approach (either we can say that the program is terminating or we cannot say anything),  our technique can identify arguments that are "limited'' (i.e., where there is no infinite propagation of terms) even when the program is not entirely recognized as terminating. Identifying arguments that are limited can support the user in the problem formulation and help other techniques that use limited arguments as a starting point. Another useful feature of our approach is that it is able to leverage external information about limited arguments. We also provide results on the correctness, the complexity, and the expressivity of our technique.


Reasonable Highly Expressive Query Languages

AAAI Conferences

Expressive query languages are gaining relevance in knowledge representation (KR), and new reasoning problems come to the fore. Especially query containment is interesting in this context. The problem is known to be decidable for many expressive query languages, but exact complexities are often missing. We introduce a new query language, guarded queries (GQ), which generalizes most known languages where query containment is decidable. GQs can be nested (more expressive), or restricted to linear recursion (less expressive). Our comprehensive analysis of the computational properties and expressiveness of (linear/nested) GQs also yields insights on many previous languages.


Temporal Query Answering in the Description Logic EL

AAAI Conferences

Context-aware systems use data collected at runtime to recognize certain predefined situations and trigger adaptations. This can be implemented using ontology-based data access (OBDA), which augments classical query answering in databases by adopting the open-world assumption and including domain knowledge provided by an ontology. We investigate temporalized OBDA w.r.t. ontologies formulated in EL, a description logic that allows for efficient reasoning and is successfully used in practice. We consider a recently proposed temporalized query language that combines conjunctive queries with the operators of propositional linear temporal logic (LTL), and study both data and combined complexity of query entailment in this setting. We also analyze the satisfiability problem in the similar formalism EL-LTL.


On the Entailment Problem for a Logic of Typicality

AAAI Conferences

Propositional Typicality Logic (PTL) is a recently proposed logic, obtained by enriching classical propositional logic with a typicality operator. In spite of the non-monotonic features introduced by the semantics adopted for the typicality operator, the obvious Tarskian definition of entailment for PTL remains monotonic and is therefore not appropriate. We investigate different (semantic) versions of entailment for PTL, based on the notion of Rational Closure as defined by Lehmann and Magidor for KLM-style conditionals, and constructed using minimality. Our first important result is an impossibility theorem showing that a set of proposed postulates that at first all seem appropriate for a notion of entailment with regard to typicality cannot be satis- fied simultaneously. Closer inspection reveals that this result is best interpreted as an argument for advocating the development of more than one type of PTL entailment. In the spirit of this interpretation, we define two primary forms of entailment for PTL and discuss their advantages and disadvantages


Partial Grounded Fixpoints

AAAI Conferences

Approximation fixpoint theory (AFT) is an algebraical study of fixpoints of lattice operators. Recently, AFT was extended with the notion of a grounded fixpoint. This type of fixpoint formalises common intuitions from various application domains of AFT, including logic programming, default logic, autoepistemic logic and abstract argumentation frameworks. The study of groundedness was limited to exact lattice points; in this paper, we extend it to the bilattice: for an approximator A of O, we define A-groundedness.  We show that all partial A-stable fixpoints are A-grounded and that the A-well-founded fixpoint is uniquely characterised as the least precise A-grounded fixpoint.  We apply our theory to logic programming and study complexity.


Compatible-Based Conditioning in Interval-Based Possibilistic Logic

AAAI Conferences

Interval-based possibilistic logic is a flexible setting extending standard possibilistic logic such that each logical expression is associated with a sub-interval of [0,1]. This paper focuses on the fundamental issue of conditioning in the interval-based possibilistic setting. The first part of the paper first proposes a set of natural properties that an interval-based conditioning operator should satisfy. We then give a natural and safe definition for conditioning an interval-based possibility distribution. This definition is based on applying standard min-based or product-based conditioning on the set of all associated compatible possibility distributions. We analyze the obtained posterior distributions and provide a precise characterization of lower and upper endpoints of the intervals associated with interpretations. The second part of the paper provides an equivalent syntactic computation of interval-based conditioning when interval-based distributions are compactly encoded by means of interval-based possibilistic knowledge bases. We show that interval-based conditioning is achieved without extra computational cost comparing to conditioning standard possibilistic knowledge bases.