Logic Programming and Nonmonotonic Reasoning

Among the challenges faced by the area of knowledge representation (KR) are the following ones: firstly, knowledge represented in different knowledge representation languages needs to be integrated, and secondly, certain applications have specific needs not typically fulfilled by standard KR systems. What we have in mind here are applications where reasoners, rather than being called by the user in order to answer some specific query, run online and have to deal with a continuous stream of information. In this paper we argue that multi-context systems (MCS) are adequate tools for both challenges. The original MCS approach was introduced to handle the integration problem in a principled way. A later extension to so-called managed MCS appears to provide relevant functionality for the second challenge. In this paper we review both MCS and managed MCS and discuss how the latter approach needs to be further developed for online applications.

Logic programming emerged in the 1970s from debates concerning procedural versus declarative representations of knowledge in artificial intelligence. In those days, declarative representations were associated mainly with bottom-up proof procedures, such as hyper-resolution. The development of logic programming showed that procedural representations could be obtained by applying top-down proof procedures, such as linear resolution, to declarative representations in logical form.

In recent years, logic programming has become more purely declarative, with the development of answer set programming, tabling and the revival of datalog. These recent developments invite comparison with earlier attempts to reconcile procedural and declarative representations of knowledge, and raise the question whether anything has been lost.

In this paper we study the relation between the two main extensions of Answer Set Programming with temporal modal operators:

Temporal Equilibrium Logic

(TEL) and

Temporal Answer Sets

(TAS). On the one hand, TEL is a complete non-monotonic logic that results from the combination of Linear-time Temporal Logic (LTL) with Equilibrium Logic. On the other hand, TAS is based on a richer modal approach, Dynamic LTL (DLTL), whereas its non-monotonic part relies on a reduct-based definition for a particular limited syntax. To integrate both approaches, we propose a Dynamic Linear-time extension of Equilibrium Logic (DTEL) that allows accommodating both TEL and TAS as particular cases. With respect to TEL, DTEL incorporates more expressiveness thanks to the addition of dynamic logic operators, whereas with respect to TAS, DTEL provides a complete non-monotonic semantics applicable to arbitrary theories. In the paper, we identify cases in which both formalisms coincide and explain how this relation can be exploited for adapting existing TEL and TAS computation methods to the general case of DTEL.

In this paper, we develop a notion of forgetting for normal logic programs under the well-founded semantics. We show that a number of desirable properties are satisfied by our approach. Three different algorithms are presented that maintain the computational complexity of the well-founded semantics, while partly keeping its syntactical structure.

Answer Set Programming is a well-established paradigm of declarative programming in close relationship with other declarative formalisms such as SAT Modulo Theories, Constraint Handling Rules, PDDL and many others. Since its first informal editions, ASP systems are compared in the nowadays customary ASP Competition. The fourth ASP Competition, held in 2012/2013, is the sequel to previous editions and it was jointly organized by University of Calabria (Italy) and the Vienna University of Technology (Austria). Participants competed on a selected collection of benchmark problems, taken from a variety of research areas and real world applications. The Competition featured two tracks: the Model& Solve Track, held on an open problem encoding, on an open language basis, and open to any kind of system based on a declarative specification paradigm; and the System Track, held on the basis of fixed, public problem encodings, written in a standard ASP language.

This paper introduces WASP, an ASP solver handling disjunctive logic programs under the stable model semantics. WASP implements techniques originally introduced for SAT solving that have been extended to cope with ASP programs. Among them are restarts, conflict-driven constraint learning and backjumping. Moreover, WASP combines these SAT-based techniques with optimization methods that have been specifically designed for ASP computation, such as source pointers enhancing unfounded-sets computation, forward and backward inference operators based on atom support, and techniques for stable model checking. Concerning the branching heuristics, WASP adopts the BerkMin criterion hybridized with look-ahead techniques. The paper also reports on the results of experiments, in which WASP has been run on the system track of the third ASP Competition.

In recent years, Answer Set Programming (ASP), logic programming under the stable model or answer set semantics, has seen several extensions by generalizing the notion of an atom in these programs: be it aggregate atoms, HEX atoms, generalized quantifiers, or abstract constraints, the idea is to have more complicated satisfaction patterns in the lattice of Herbrand interpretations than traditional, simple atoms. In this paper we refer to any of these constructs as generalized atoms. It is known that programs with generalized atoms that have monotonic or antimonotonic satisfaction patterns do not increase complexity with respect to programs with simple atoms (if satisfaction of the generalized atoms can be decided in polynomial time) under most semantics. It is also known that generalized atoms that are nonmonotonic (being neither monotonic nor antimonotonic) can, but need not, increase the complexity by one level in the polynomial hierarchy if non-disjunctive programs under the FLP semantics are considered. In this paper we provide the precise boundary of this complexity gap: programs with convex generalized atom never increase complexity, while allowing a single non-convex generalized atom (under reasonable conditions) always does. We also discuss several implications of this result in practice.

Answer set programming (ASP) is nowadays one of the most popular modeling languages in the areas of Knowledge Representation and Artificial Intelligence. Hereby one represents the problem at hand in such a way that each model of the ASP program corresponds to one solution of the original problem. In recent years, several tools which support the user in developing ASP applications have been introduced. However, explicit treatment of one of the main aspects of ASP, multiple solutions, has received less attention within these tools. In this work, we present a novel system to visualize

relations

between answer sets of a given program. The core idea of the system is that the user specifies the concept of a relation by an ASP program itself. This yields a highly flexible system that suggests potential applications beyond development environments, e.g., applications in the field of abduction, which we will discuss in a case study.

Recently, Boolean Satisfiability (SAT) solving has been proposed to tackle the increasing complexity in high-level system design. Working well for system specifications with a limited amount of routing options, they tend to fail for densely connected computing platforms. This paper proposes an automated system design approach employing Answer Set Programming (ASP). ASP provides a stringent semantics, allowing for an efficient representation of routing options. An automotive case-study illustrates that the proposed ASP-based system design approach is competitive for sparsely connected computing platforms, while it outperforms SAT-based approaches for dense Networks-on-Chip by an order of magnitude.

Precise knowledge of the longest sensitizable paths in a circuit is crucial for various tasks in computer-aided design, including timing analysis, performance optimization, delay testing, and speed binning. As delays in today’s nanoscale technologies are increasingly affected by statistical parameter variations, there is significant interest in obtaining sets of paths that are within a length range. For instance, such path sets can be used in the emerging areas of

Post-silicon validation and characterization

and

Adaptive Test

. We present an ASP-based method for computing well-defined sets of sensitizable paths within a length range. Unlike previous approaches, the method is accurate and does not rely on a priori relaxations. Experimental results demonstrate the applicability and scalability of our method.

Approximation Fixpoint Theory (AFT) is an algebraic framework for studying fixpoints of possibly nonmonotone lattice operators, and thus extends the fixpoint theory of Tarski and Knaster. In this paper, we uniformly define 2-, and 3-valued (ultimate) answer-set semantics, and well-founded semantics of disjunction-free

Hex

programs by applying AFT. In the case of disjunctive

Hex

programs, AFT is not directly applicable. However, we provide a definition of 2-valued (ultimate) answer-set semantics based on non-deterministic approximations and show that answer sets are minimal, supported, and derivable in terms of bottom-up computations. Finally, we extensively compare our semantics to closely related semantics, including constructive dl-program semantics. Since

Hex

programs are a generic formalism, our results are applicable to a wide range of formalisms.

Answering realistic questions about biological systems and pathways similar to text book questions used for testing students’ understanding of such systems is one of our long term research goals. Often these questions require simulation based reasoning. In this paper, we show how higher level extensions of Petri Nets, such as colored tokens can be encoded in Answer Set Programming, thereby providing the right formalisms to model and reason about such questions with relative ease. Our approach can be adapted to other domains.

We present Version 2 of system

Cplus2ASP

, which implements the definite fragment of action language

${\cal C}$

+. Its input language is fully compatible with the language of the Causal Calculator Version 2, but the new system is significantly faster thanks to modern answer set solving techniques. The translation implemented in the system is a composition of several recent theoretical results. The system orchestrates a tool chain, consisting of

f2lp

,

clingo

,

iclingo

, and

as2transition

. Under the incremental execution mode, the system translates a

${\cal C}$

+ description into the input language of

iclingo

, exploiting its incremental grounding mechanism. The correctness of this execution is justified by the module theorem extended to programs with nested expressions. In addition, the input language of the system has many useful features, such as external atoms by means of Lua calls and the user interactive mode. The system supports extensible multi-modal translations for other action languages, such as

${\cal B}$

and

${\cal BC}$

, as well.

Existing ASP languages lack support for conveniently specifying objects, their sorts and the sorts of the parameters of relations in an application domain. However, such support may allow a programmer to better structure the program, to automatically determine some syntax and semantic errors and to avoid thinking about safety of ASP rules — non-declarative conditions on rules required by existing ASP systems. In this paper, we define the syntax and semantics of a knowledge representation language

$\mathcal{SPARC}$

which offers explicit constructs to specify objects, relations, and their sorts. The language expands CR-Prolog — an extension of ASP by consistency restoring rules. We introduce an implementation of

$\mathcal{SPARC}$

based on its translation to DLV with weak constraints. A syntax checking algorithm helps to avoid errors related to misspellings as well as simple type errors. Another type checking algorithm flags program rules which, due to type conflicts, have no ground instantiations.

Answer set programming (ASP) is a declarative programming paradigm stemming from logic programming that has been successfully applied in various domains. Despite amazing advancements in ASP solving, many applications still pose a challenge that is commonly referred to as

grounding bottleneck

. Devising, implementing, and evaluating a method that alleviates this problem for certain application domains is the focus of this paper. The proposed method is based on combining backtracking-based search algorithms employed in answer set solvers with SLDNF resolution from

prolog

. Using

prolog

inference on non-ground portions of a given program, both grounding time and the size of the ground program can be substantially reduced.

The broader goal of our research is to formulate answers to why and how questions with respect to knowledge bases, such as AURA. One issue we face when reasoning with many available knowledge bases is that at times needed information is missing. Examples of this include partially missing information about next sub-event, first sub-event, last sub-event, result of an event, input to an event, destination of an event, and raw material involved in an event. In many cases one can recover part of the missing knowledge through reasoning. In this paper we give a formal definition about how such missing information can be recovered and then give an ASP implementation of it. We then discuss the implication of this with respect to answering why and how questions.

We report on preliminary research towards native algorithms for query answering over relational nonmonotonic Multi-Context Systems (MCS), i.e., algorithms that do not rely on computing equilibria. Inspired by techniques for query answering in distributed answer set programming, we identify MCS settings where a generalized query answering algorithm is effective and efficient; confirmed by a preliminary evaluation on a real world application.

In this paper we present various new results related to the dynamics of abstract argumentation. Baumann [1] studied the effort needed to enforce a set of arguments

E

, measured in terms of the minimal number of modifications needed to turn an argumentation framework (AF)

$\mathcal{A}$

into a framework

$\mathcal{A}^*$

such that

$\mathcal{A}^*$

has an extension containing

E

. This value, called the characteristic, depends on the chosen semantics and the type of admitted modifications. Here we study the inverse problem (called the

spectrum problem

): given a collection of semantics and a modification type, what are the corresponding tuples of characteristics one may obtain for an arbitrary argumentation framework

$\mathcal{A}$

and set of arguments

E

? The set of all these tuples is called the spectrum. We define various properties of spectra and show that the investigation of spectra reveals interesting and surprising insights into the relationship among several semantics.

Answer-set programs become more expressive if extended by cardinality rules. Certain implementation techniques, however, presume the translation of such rules back into normal rules. This has been previously realized using a BDD-based transformation which may produce a quadratic number of rules in the worst case. In this paper, we present two further constructions which are based on Boolean circuits for merging and sorting and which have been considered, e.g., in the context of the propositional satisfiability (SAT) problem and its extensions. Such circuits can be used to express cardinality constraints in a more compact way. Thus, in order to normalize cardinality rules, we first develop an ASP encoding of a sorting circuit, on top of which the second translation, one encoding a selection circuit, is devised. Because sorting is more general than cardinality checking, we also present ways to prune the resulting sorting and selection programs. The experimental part illustrates the compactness of the new normalizations and points out cases where computational performance is improved.

Within everyday reasoning we often use argumentation patterns that employ the rather vague notion of something being

normally true

. This form of reasoning is usually captured using Reiter’s Default Logic. However, in Default Logic one has to make explicit the rules which are to be used for reasoning and which are supposed to be normally true. This is a bit contrary to the everyday situation where people use

experience

to decide what normally follows from particular observations and what not, not using any kind of logical rules at all. To formalize this kind of reasoning we propose an approach which is based on

prior experiences

, using the fact that something follows normally if this is the case for “almost all” of the available experience.

Integrating heterogeneous knowledge is necessary to elucidate the regulations in biological systems. In particular, such an integration is widely used to identify functional units, that are sets of genes that can be triggered by the same external stimuli, as biological stresses, and that are linked to similar responses of the system. Although several models and algorithms shown great success for detecting functional units on well-known biological species, they fail in identifying them when applied to more exotic species, such as extremophiles, that are by nature unrefined. Indeed, approved methods on unrefined models suffer from an explosion in the number of solutions for functional units, that are merely combinatorial variations of the same set of genes. This paper overcomes this crucial limitation by introducing the concept of “genome segments”. As a natural extension of recent studies, we rely on the declarative modeling power of answer set programming (ASP) to encode the identification of shortest genome segments (SGS). This study shows, via experimental evidences, that SGS is a new model of functional units with a predictive power that is comparable to existing methods. We also demonstrate that, contrary to existing methods, SGS are stable in (i) computational time and (ii) ability to predict functional units when one deteriorates the biological knowledge, which simulates cases that occur for exotic species.

In games with imperfect information, the ‘information set’ is a collection of all possible game histories that are consistent with, or explain, a player’s observations. Current game playing systems rely on these best guesses of the true, partially-observable game as the foundation of their decision making, yet finding these information sets is expensive.

We apply reactive Answer Set Programming (ASP) to the problem of sampling information sets in the field of General Game Playing. Furthermore, we use this domain as a test bed for evaluating the effectiveness of oClingo, a reactive answer set solver, in avoiding redundant search by keeping learnt clauses during incremental solving.

System competitions evaluate solvers and compare state-of-the-art implementations on benchmark sets in a dedicated and controlled computing environment, usually comprising of multiple machines. Recent initiatives such as [6] aim at establishing best practices in computer science evaluations, especially identifying measures to be taken for ensuring repeatability, excluding common pitfalls, and introducing appropriate tools. For instance, Asparagus [1] focusses on maintaining benchmarks and instances thereof. Other known tools such as Runlim (http://fmv.jku.at/runlim/) and Runsolver [12] help to limit resources and measure CPU time and memory usage of solver runs. Other systems are tailored at specific needs of specific communities: the not publicly accessible ASP Competition evaluation platform for the 3rd ASP Competition 2011 [4] implements a framework for running a ASP competition. Another more general platform is StarExec [13], which aims at providing a generic framework for competition maintainers. The last two systems are similar in spirit, but each have restrictions that reduce the possibility of general usage: the StarExec platform does not provide support for generic solver input and has no scripting support, while the ASP Competition evaluation platform has no support for fault-tolerant execution of instance runs.Moreover, benchmark statistics and ranking can only be computed after all solver runs for all benchmark instances have been completed.

This paper presents a sequential model of bargaining based on abductive reasoning in ASP. We assume that each agent is represented by a logic program that encodes the background knowledge of the agent. Each agent has a set of goals to achieve but these goals are normally unachievable without an agreement from the other agent. We design an alternating-offers procedure that shows how an agreement between two agents can be reached through a reasoning process based on answer set programming and abduction. We prove that the procedure converges to a Nash equilibrium if each player makes rational offer/counter-offer at each round.

Metabolic network reconstruction is of great biological relevance because it offers a way to investigate the metabolic behavior of organisms. However, reconstruction remains a difficult task at both the biological and computational level. Building on previous work establishing an ASP-based approach to this problem, we present a report from the field resulting in the discovery of new biological knowledge. In fact, for the first time ever, we automatically reconstructed a metabolic network for a macroalgae. We accomplished this by taking advantage of ASP’s combined optimization and enumeration capacities. Both computational tasks build on an improved ASP problem representation, incorporating the concept of reversible reactions. Interestingly, optimization greatly benefits from the usage of unsatisfiable cores available in the ASP solver

unclasp

. Applied to

Ectocarpus siliculosus

, only the combination of

unclasp

and

clasp

allowed us to obtain a metabolic network able to produce all recoverable metabolites among the experimentally measured ones. Moreover, 70% of the identified reactions are supported by an homologous enzyme in

Ectocarpus siliculosus

, confirming the quality of the reconstructed network from a biological viewpoint.

In recent work, we provided a formulation of ASP programs in terms of linear logic theories. Based on this work, in this paper we propose and discuss a modified Answer Set Semantics, “Resource-based Answer Set Semantics”.

In the past few years, several approaches for revision (and update) of logic programs have been studied. None of these however matched the generality and elegance of the original AGM approach to revision in classical logic. One particular obstacle is the underlying nonmonotonicity of the semantics of logic programs. Recently however, specific revision operators based on the monotonic concept of SE-models (which underlies the answer-set semantics of logic programs) have been proposed. Basing revision of logic programs on sets of SE-models has the drawback that arbitrary sets of SE-models may not necessarily be expressed via a logic program. This situation is similar to the emerging topic of revision in fragments of classical logic. In this paper we show how nonetheless classical AGM-style revision can be extended to various classes of logic programs using the concept of SE-models. That is, we rephrase the AGM postulates in terms of logic programs, provide a semantic construction for revision operators, and then in a representation result show that these approaches coincide. This work is interesting because, on the one hand it shows how the AGM approach can be extended to a seemingly nonmonotonic framework, while on the other hand the formal characterization may provide guiding principles for the development of specific revision operators.

Many native ASP solvers exploit unfounded sets to compute consequences of a logic program via some form of well-founded negation, but disregard its contrapositive, well-founded justification (WFJ), due to computational cost. However, we demonstrate that this can hinder propagation of many relevant conditions such as reachability. In order to perform WFJ with low computational cost, we devise a method that approximates its consequences by computing dominators in a flowgraph, a problem for which linear-time algorithms exist. Furthermore, our method allows for additional unfounded set inference, called well-founded domination (WFD). We show that the effect of WFJ and WFD can be simulated for a important classes of logic programs that include reachability. Finally, we take a stand for native ASP solvers and show that unfounded set inference cannot be replaced by logic program transformations or translations into CNF-SAT.

We propose a history-based approximation of the Possible Worlds Semantics (

$\mathcal{PWS}$

) for reasoning about knowledge and action. A respective planning system is implemented by a transformation of the problem domain to an Answer-Set Program. The novelty of our approach is elaboration tolerant support for postdiction under the condition that the plan existence problem is still solvable in NP, as compared to

$\Sigma_2^P$

for non-approximated

$\mathcal{PWS}$

of [20]. We demonstrate our planner with standard problems and present its integration in a cognitive robotics framework for high-level control in a smart home.

We extend the language of here-and-there logic by two kinds of atomic programs allowing to minimally update the truth value of a propositional variable here or there, if possible. These atomic programs are combined by the usual dynamic logic program connectives. We investigate the mathematical properties of the resulting extension of equilibrium logic: we prove that the problem of logical consequence in equilibrium models is EXPTIME complete by relating equilibrium logic to dynamic logic of propositional assignments.

acthex

programs are a convenient tool for connecting stateful external environments to logic programs. In the

acthex

framework, actual actions on an external environment can be declaratively selected, rearranged, scheduled and then executed depending on intelligence specified in an ASP-based language. We report in this paper about recent improvements of the formal and of the operational

acthex

programming framework. Besides yielding a significant increase in versatility of the framework, we also present illustrative application showcases and a short evaluation thereof exhibiting computational

acthex

strengths.

In answer-set programming (ASP), there is a lack of debugging tools that are capable of handling programs with variables. Hence, we implemented a tool, called

Ouroboros

, for debugging non-ground answer-set programs. The system builds on a previous approach based on ASP meta-programming that has been recently extended to cover weight constraints and choice rules. The main debugging question addressed is “given a program

P

and an interpretation

I

, why is

I

not an answer set of

P

”. Our tool gives answers in terms of two categories of explanations: unsatisfied rules and unfounded loops.

Ouroboros

is a plugin of the

SeaLion

integrated development environment for ASP that is built on Eclipse. Thereby,

Ouroboros

complements and profits from

SeaLion

’s

Stepping

plugin, that implements a different debugging approach for ASP.

Intensional logic programming

is an extension of logic programming based on intensional logic, which includes as special cases both

temporal

and

modal

logic programming. In [OW92], M. Orgun and W. W. Wadge provided a general framework for capturing the semantics of intensional logic programming languages. One key property involved in the construction of [OW92], is the

monotonicity

of intensional operators. In this paper we consider intensional logic programming from a game-theoretic perspective. In particular we define a two-person game and we demonstrate that it is equivalent to the semantics of [OW92]. More importantly, we demonstrate that the game is even applicable to intensional languages with

non-monotonic

operators. In this way we provide the first (to our knowledge) general semantic framework for capturing the semantics of non-monotonic intensional logic programming.

Matchmaking is a form of scheduling that aims at bringing companies or people together that share common interests, services, or products in order to facilitate future business partnerships.We begin by furnishing a formal characterization of the corresponding multi-criteria optimization problem.We then address this problem by Answer Set Programming in order to solve real-world matchmaking instances, which were previously dealt with by special-purpose algorithms.

A distinguishing feature of Answer Set Programming is its versatility. In addition to satisfiability testing, it offers various forms of model enumeration, intersection or unioning, as well as optimization. Moreover, there is an increasing interest in incremental and reactive solving due to their applicability to dynamic domains. However, so far no comparative studies have been conducted, contrasting the respective modeling capacities and their computational impact. To assess the variety of different forms of ASP solving, we propose Alex Randolph’s board game

Ricochet Robots

as a transverse benchmark problem that allows us to compare various approaches in a uniform setting. To begin with, we consider alternative ways of encoding ASP planning problems and discuss the underlying modeling techniques. In turn, we conduct an empirical analysis contrasting traditional solving, optimization, incremental, and reactive approaches. In addition, we study the impact of some boosting techniques in the realm of our case study.

Parametrized logic programs are very expressive logic programs that generalize normal logic programs under the stable model semantics, by allowing complex formulas of a parameter logic to appear in the body and head of rules. In this paper we study the decidability of these rich programs and propose an implementation that combines, in a modular way, a reasoner for the parameter logic with an answer set solver.

In this paper we introduce a logic programming based framework which allows the representation of conditional non-monotonic temporal beliefs and goals in a declarative way. We endow it with stable model like semantics that allows us to deal with conflicting goals and generate possible alternatives. We show that our framework satisfies some usual properties on goals and that it allows imposing alternative constraints on the interaction between beliefs and goals. We prove the decidability of the usual reasoning tasks and show how they can be implemented using an ASP solver and an LTL reasoner in a modular way, thus taking advantage of existing LTL reasoners and ASP solvers.

It has been known for a long time that intuitionistically equivalent formulas have the same stable models. We extend this theorem to propositional formulas with infinitely long conjunctions and disjunctions and show how to apply this generalization to proving properties of aggregates in answer set programming.

This paper explores the contributions of Answer Set Programming (ASP) to the study of an established theory from the field of Second Language Acquisition: Input Processing. The theory describes default strategies that learners of a second language use in extracting meaning out of a text, based on their knowledge of the second language and their background knowledge about the world. We formalized this theory in ASP, and as a result we were able to determine opportunities for refining its natural language description, as well as directions for future theory development. We applied our model to automating the prediction of how learners of English would interpret sentences containing the passive voice. We present a system,

PIas

, that uses these predictions to assist language instructors in designing teaching materials.

Turner’s logic of universal causation is a general logic for nonmonotonic reasoning. It has its origin in McCain and Turner’s causal action theories which have been translated to propositional logic and logic programming with nested expressions. In this paper, we propose to do the same for Turner’s logic, and show thatTurner’s logic can actually be mapped to McCain and Turner’s causal theories. These results can be used to construct a system for reasoning in Turner’s logic.

There are many different notions of “rule” in the literature. A key feature and main intuition of any such notion is that rules can be “applied” to derive conclusions from certain premises. More formally, a rule is viewed as a function that, when invoked on a set of known facts, can produce new facts. In this paper, we show that this extreme simplification is still sufficient to obtain a number of useful results in concrete cases. We define abstract rules as a certain kind of functions, provide them with a semantics in terms of (abstract) stable models, and explain how concrete normal logic programming rules can be viewed as abstract rules in a variety of ways. We further analyse dependencies between abstract rules to recognise classes of logic programs for which stable models are guaranteed to be unique.

In this paper, we explore the use of Linear Logic programming for story generation. We use the language Celf to represent narrative knowledge, and its own querying mechanism to generate story instances, through a number of proof terms. Each proof term obtained is used, through a resource-flow analysis, to build a directed graph where nodes are narrative actions and edges represent inferred causality relationships. Such graphs represent narrative plots structured by narrative causality. This approach is a candidate technique for narrative generation which unifies declarative representations and generation via query and deduction mechanisms.

We describe a system that, given a theory of an answer-set programming (ASP) system

psgrnd

, generates its informal reading in natural language. That reading helps understand the

psgrnd

theory, and verify its correctness or identify programming errors. Similar tools can be developed for other ASP formalisms. To this end, the basic language used by the system has to be extended to allow the programmer provide (minimal) additional information on how to understand atomic concepts, of which the theory (program) is built.

Accounts of belief and knowledge in the Situation Calculus have been developed and discussed for some time yet there is no extant implementation. We develop a practical implementation of belief and belief change in the Situation Calculus based on default logic for which we have an implemented solver. After establishing the mapping with default logic we demonstrate how belief change in the Situation Calculus can be used to solve an interesting problem in robotics – reasoning with misleading information. Motivated by a challenge in the RoboCup@Home competition, we give a solution to the problem of planning robustly in cases where operators provide the robot with misleading or incorrect information.

When deploying Answer Set Programming (ASP) in an industrial context, for instance for (re-)configuration [5], knowledge engineers need debugging support on non-ground programs. Current approaches to ASP debugging, however, do not cover extended modeling features of ASP, such as choice rules, conditional literals, cardinality and weight constraints [13]. To this end, we encode non-ground ASP programs using extended modeling features into normal logic progams; this encoding extends existing encodings for the case of ground programs [4,10,11] to the non-ground case. We subsequently deploy this translation on top of an existing ASP debugging approach for non-ground normal logic programs [14]. We have implemented and tested the approach and provide evaluation results.

Many real-world design problems such as product configuration require a flexible number of components and thus rely on tuple generating dependencies in order to express relations between entities. Often, such problems are subject to optimization, preferring models which include a minimal number of constants substituted in existentially quantified formulas.

In this paper we propose an approach based on automated program rewriting which avoids such substitutions of existentially quantified variables that would lead to a contradiction. While preserving all solutions, the method significantly reduces runtime and solves instances of a class of real-world configuration problems which could not be efficiently solved by current techniques.

We propose a novel conceptual approach to program updates implementation that exploits two features of tabling in logic programming (in XSB Prolog): incremental and answer subsumption tabling. Our approach, EVOLP/R, is based on the constructs of Evolving Logic Programs (EVOLP), but simplifies it at first by restricting updates to fluents only. Rule updates are nevertheless achieved via the mechanism of rule name fluents, placed in rules’ bodies, permitting to turn rules on or off, through assertions or retractions of their corresponding unique name fluents. Incremental tabling of fluents allows to automatically maintain – at engine level – the consistency of program states. Answer subsumption of fluents addresses the frame problem – at engine level – by automatically keeping track of their latest assertion or retraction. The implementation is detailed here to the extent that it may be exported to other logic programming tabling systems.

We address the problem of belief revision of logic programs, i.e., how to incorporate to a logic program

$\mathcal{P}$

a new logic program

$\mathcal{Q}$

. Based on the structure of SE interpretations, Delgrande

et al.

[5] adapted the AGM postulates to identify the rational behavior of

generalized

logic program (GLP) revision operators and introduced some specific operators. In this paper, a constructive characterization of

all

rational GLP revision operators is given in terms of an ordering among propositional interpretations with some further conditions specific to SE interpretations. It provides an intuitive, complete procedure for the construction of all rational GLP revision operators and makes easier the comprehension of their semantic properties. In particular, we show that every rational GLP revision operator is derived from a propositional revision operator satisfying the original AGM postulates. Taking advantage of our characterization, we embed the GLP revision operators into structures of Boolean lattices, that allow us to bring to light some potential weaknesses in the adapted AGM postulates. To illustrate our claim, we introduce and characterize axiomatically two specific classes of (rational) GLP revision operators which arguably have a drastic behavior.

Combinatory Categorial Grammar (CCG) is a grammar formalism used for natural language parsing. CCG assigns structured lexical categories to words and uses a small set of combinatory rules to combine these categories in order to parse sentences. In this work we describe and implement a new approach to CCG parsing that relies on Answer Set Programming (ASP) — a declarative programming paradigm.Different from previous work, we present an encoding that is inspired by the algorithm due to Cocke, Younger, and Kasami (CYK). We also show encoding extensions for parse tree normalization and best-effort parsing and outline possible future extensions which are possible due to the usage of ASP as computational mechanism. We analyze performance of our approach on a part of the Brown corpus and discuss lessons learned during experiments with the ASP tools dlv, gringo, and clasp. The new approach is available in the open source CCG parsing toolkit AspCcgTk which uses the C&C supertagger as a preprocessor to achieve wide-coverage natural language parsing.

We pinpoint the limitations of existing approaches to the treatment of

strong

and

default negation

in answer-set program updates and formulate the

early recovery principle

that plausibly constrains their interaction.

We introduce an approach to preferences suitable for agents that base decisions on their beliefs. In our work, agents’ preferences are perceived as a consequence of their beliefs, but at the same time are used to feed the knowledge base with beliefs about preferences. As a result, agents can reason with preferences to hypothesize, explain decisions, and review preferences in face of new information. Finally, we integrate utility-based to reasoning-based criteria of decision making.

In this paper we present a technique based on logic programming for data cleaning, and its application to a real use case from the Italian Healthcare System. The use case is part of a more complex project developing a business intelligence suite for the analysis of distributed archives of tumor-based diseases.

Understanding why and how a given answer to a query is generated from a deductive or relational database is fundamental to obtain justifications, assess trust, and detect dependencies on contradictions. Propagating provenance information is a major technique that evolved in the database literature to address the problem, using annotated relations with values from a semiring. The case of positive programs/relational algebra is well-understood but handling negation (or set difference in relational algebra) has not been addressed in its full generality or has deficiencies. The approach defined in this work provides full provenance information for logic programs under the least model, well-founded semantics and answer set semantics, and is related to the major existing notions of justifications for all these logic programming semantics.

Brewka and Eiter’s nonmonotonic multi-context system is an elegant knowledge representation framework to model heterogeneous and nonmonotonic multiple contexts. Belief change is a central problem in knowledge representation and reasoning. In this paper we follow the classical AGM approach to investigate belief change in multi-context systems. Specifically, we formulate semantically the AGM postulates of belief expansion, revision and contraction for multi-context systems. We show that the change operations can be characterized in terms of minimal change by ordering equilibria of multi-context systems. Two distance based revision operators are obtained and related to the classical Satoh and Dalal revision operators (via loop formulas).

In 2003, Brewka, Niemelä and Truszczynski introduced answer-set optimization problems. They consist of two components: a logic program and a set of preference rules. Answer sets of the program represent possible outcomes; preferences determine a preorder on them. Of interest are answer sets of the program that are optimal with respect to the preferences. In this work, we consider computational problems concerning optimal answer sets. We implement and study several methods for the problems of computing an optimal answer set; computing another one, once the first one is found; and computing an optimal answer set that is similar to (respectively, dissimilar from) a given interpretation. For the problems of the existence of similar and dissimilar optimal answer set we establish their computational complexity.