Autonomous vehicles are complex distributed systems consisting of multiple software applications and computing nodes. Determining the assignment between these software applications and computing nodes is known as the application-placement problem. The input of this problem is a set of applications, their requirements, a set of computing nodes, and their provided resources. Due to the potentially large solution space of the problem, an optimization goal defines which solution is desired the most. However, the optimization goal used for the application-placement problem is not static but has to be adapted according to the current context the vehicle is experiencing. Therefore, an approach for a context-based determination of the optimization goal for a given instance of an application-placement problem is required. In this paper, we introduce C-po, an approach to address this issue. C - PO ensures that if the safety level of a system drops due to an occurring failure, the optimization goal for the successively executed application-placement determination aims to restore the safety level. Once the highest safety level is reached, C-po optimizes the application placement according to the current driving situation. Furthermore, we introduce two methods for dynamically determining the required level of safety.

This article deals with advanced notions of equivalence between nonmonotonic logic programs under the answer-set semantics, a topic of considerable interest, because such notions form the basis for program verification and are useful for program optimisation, debugging, and modular programming. In fact, there is extensive research in answer-set programming (ASP) dealing with different notions of equivalence between programs. Prominent among these notions is uniform equivalence , which checks whether two programs have the same semantics when joined with an arbitrary set of facts. In this article, we study a family of more fine-grained versions of uniform equivalence, viz. relativised uniform equivalence with projection , which extends standard uniform equivalence in terms of two additional parameters: one for specifying the input alphabet and one for specifying the output alphabet for programs. In particular, the second parameter is used for projecting answer sets to a set of designated output atoms. Answer-set projection, in particular, allows to compare programs that make use of different auxiliary atoms, which is important for practical programming aspects. We introduce novel semantic characterisations for the program correspondence problems under consideration and analyse their computational complexity. In the general case, deciding these problems lies on the third level of the polynomial hierarchy. Therefore, this task cannot be efficiently reduced to propositional answer-set programs itself (under the usual complexity-theoretic assumptions). However, reductions to quantified Boolean formulas (QBFs) are feasible. Indeed, we provide efficient (in fact, linear-time constructible) reductions to QBFs and discuss simplifications for certain special cases. These QBF reductions yield the basis for a prototype implementation, the system cc ⊤, for deciding correspondence problems by using off-the-shelf QBF solvers. We discuss an application of cc ⊤ for verifying the correctness of solutions by students drawn from a laboratory course on logic programming and knowledge representation at the Technische Universität Wien, employing relativised uniform equivalence with projection as the underlying program correspondence notion.

Abstract We introduce astepping methodologyfor answer-set programming (ASP) that allows for debugging answer-set programs and is based on the stepwise application of rules. Similar to debugging in imperative languages, where the behaviour of a program is observed during a step-by-step execution, stepping for ASP allows for observing the effects that rule applications have in the computation of an answer set. While the approach is inspired from debugging in imperative programming, it is conceptually different to stepping in other paradigms due to non-determinism and declarativity that are inherent to ASP. In particular, unlike statements in an imperative program that are executed following a strict control flow, there is no predetermined order in which to consider rules in ASP during a computation. In our approach, the user is free to decide which rule to consider active in the next step following his or her intuition. This way, one can focus on interesting parts of the debugging search space. Bugs are detected during stepping by revealing differences between the actual semantics of the program and the expectations of the user. As a solid formal basis for stepping, we develop a framework of computations for answer-set programs. For fully supporting different solver languages, we build our framework on an abstract ASP language that is sufficiently general to capture different solver languages. To this end, we make use of abstract constraints as an established abstraction for popular language constructs such as aggregates. Stepping has been implemented inSeaLion, an integrated development environment for ASP. We illustrate stepping using an example scenario and discuss the stepping plugin ofSeaLion. Moreover, we elaborate on methodological aspects and the embedding of stepping in the ASP development process.

Clause-elimination techniques that simplify formulas by removing redundant clauses play an important role in modern SAT solving. Among the types of redundant clauses, blocked clauses are particularly popular. For checking whether a clause C is blocked in a formula F, one only needs to consider the so-called resolution neighborhood of C, i.e., the set of clauses that can be resolved with C. Because of this, blocked clauses are referred to as being locally redundant. In this paper, we discuss powerful generalizations of blocked clauses that are still locally redundant, viz. set-blocked clauses and super-blocked clauses. We furthermore present complexity results for deciding whether a clause is set-blocked or super-blocked.

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses whose elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.

We address the problem of belief change in (nonmonotonic) logic programming under answer set semantics. Our formal techniques are analogous to those of distance-based belief revision in propositional logic. In particular, we build upon the model theory of logic programs furnished by SE interpretations, where an SE interpretation is a model of a logic program in the same way that a classical interpretation is a model of a propositional formula. Hence we extend techniques from the area of belief revision based on distance between models to belief change in logic programs. We first consider belief revision: for logic programs P and Q , the goal is to determine a program R that corresponds to the revision of P by Q , denoted P * Q . We investigate several operators, including (logic program) expansion and two revision operators based on the distance between the SE models of logic programs. It proves to be the case that expansion is an interesting operator in its own right, unlike in classical belief revision where it is relatively uninteresting. Expansion and revision are shown to satisfy a suite of interesting properties; in particular, our revision operators satisfy all or nearly all of the AGM postulates for revision. We next consider approaches for merging a set of logic programs, P 1 , ..., P n . Again, our formal techniques are based on notions of relative distance between the SE models of the logic programs. Two approaches are examined. The first informally selects for each program P i those models of P i that vary the least from models of the other programs. The second approach informally selects those models of a program P 0 that are closest to the models of programs P 1 , ..., P n . In this case, P 0 can be thought of as a set of database integrity constraints. We examine these operators with regards to how they satisfy relevant postulate sets. Last, we present encodings for computing the revision as well as the merging of logic programs within the same logic programming framework. This gives rise to a direct implementation of our approach in terms of off-the-shelf answer set solvers. These encodings also reflect the fact that our change operators do not increase the complexity of the base formalism.

Abstract In this paper, we present SeaLion, an integrated development environment (IDE) for answer-set programming (ASP). SeaLion provides source-code editors for the languages of Gringo and DLV and offers popular amenities like syntax highlighting, syntax checking, code completion, visual program outline, and refactoring functionality. The tool has been realised in the context of a research project whose goal is the development of techniques to support the practical coding process of answer-set programs. In this respect, SeaLion is the first IDE for ASP that provides debugging features that work for real-world answer-set programs and supports the rich languages of modern answer-set solvers. Indeed, SeaLion implements a stepping-based debugging approach that allows the developer to quickly track down programming errors by simply following his or her intuitions on the intended semantics. Besides that, SeaLion supports ASP development using model-driven engineering techniques including domain modelling with extended UML class diagrams and visualisation of answer sets in corresponding instance diagrams. Moreover, customised visualisation as well as visual editing of answer sets is realised by the Kara plugin of SeaLion. Further implemented features are a documentation generator based on the Lana annotation language, support for external solvers, and interoperability with external tools. SeaLion comes as a plugin of the popular Eclipse platform and provides interfaces for future extensions of the IDE.

Abstract While past research in answer-set programming (ASP) mainly focused on theory, ASP solver technology, and applications, the present work situates itself in the context of a quite recent research trend: development support for ASP. In particular, we propose to augment answer-set programs with additional meta-information formulated in a dedicated annotation language, called Lana. This language allows the grouping of rules into coherent blocks and to specify language signatures, types, pre- and postconditions, as well as unit tests for such blocks. While these annotations are invisible to an ASP solver, as they take the form of program comments, they can be interpreted by tools for documentation, testing, and verification purposes, as well as to eliminate sources of common programming errors by realising syntax checking or code completion features. To demonstrate its versatility, we introduce two such tools, viz. (i) ASPDoc, for generating an HTML documentation for a program based on the annotated information, and (ii) ASPUnit, for running and monitoring unit tests on program blocks. Lana is also exploited in the SeaLion system, an integrated development environment for ASP based on Eclipse.

In the context of the Semantic Web, several approaches for combining ontologies, given in terms of theories of classical first-order logic and rule bases, have been proposed. They either cast rules into classical logic or limit the interaction between rules and ontologies. Autoepistemic logic (AEL) is an attractive formalism which allows overcoming these limitations by serving as a uniform host language to embed ontologies and nonmonotonic logic programs into it. For the latter, so far only the propositional setting has been considered. In this article, we present three embeddings of normal and three embeddings of disjunctive nonground logic programs under the stable model semantics into first-order AEL. While all embeddings correspond with respect to objective ground atoms, differences arise when considering nonatomic formulas and combinations with first-order theories. We compare the embeddings with respect to stable expansions and autoepistemic consequences, considering the embeddings by themselves, as well as combinations with classical theories. Our results reveal differences and correspondences of the embeddings, and provide useful guidance in the choice of a particular embedding for knowledge combination.

Answer-set programming (ASP) is a well-acknowledged paradigm for declarative problem solving, yet comparably little effort has been spent on the investigation of methods to support the development of answer-set programs. In particular, systematic testing of programs, constituting an integral part of conventional software development, has not been discussed for ASP thus far. In this paper, we fill this gap and develop notions enabling the structural testing of answer-set programs, i.e., we address testing based on test cases that are chosen with respect to the internal structure of a given answer-set program. More specifically, we introduce different notions of coverage that measure to what extent a collection of test inputs covers certain important structural components of the program. In particular, we introduce metrics corresponding to path and branch coverage from conventional testing. We also discuss complexity aspects of the considered notions and give strategies how test inputs that yield increasing (up to total) coverage can be automatically generated.

Abstract Plagiarism detection is a growing need among educational institutions and solutions for different purposes exist. An important field in this direction is detecting cases of source-code plagiarism. In this paper, we present the tool Kato for supporting the detection of this kind of plagiarism in the area of answer-set programming (ASP). Currently, the tool is implemented for DLV programs but it is designed to handle other logic-programming dialects as well. We review the basic features of Kato, introduce its theoretical underpinnings, and discuss an application of Kato for plagiarism detection in the context of courses on logic programming at the Vienna University of Technology.

Abstract An important issue towards a broader acceptance of answer-set programming (ASP) is the deployment of tools which support the programmer during the coding phase. In particular, methods fordebuggingan answer-set program are recognised as a crucial step in this regard. Initial work on debugging in ASP mainly focused on propositional programs, yet practical debuggers need to handle programs with variables as well. In this paper, we discuss a debugging technique that is directly geared towards non-ground programs. Following previous work, we address the central debugging question why some interpretation is not an answer set. The explanations provided by our method are computed by means of a meta-programming technique, using a uniform encoding of a debugging request in terms of ASP itself. Our method also permits programs containing comparison predicates and integer arithmetics, thus covering a relevant language class commonly supported by all state-of-the-art ASP solvers.

Practically all programming languages allow the programmer to split a program into several modules which brings along several advantages in software development. In this paper, we are interested in the area of answer-set programming where fully declarative and nonmonotonic languages are applied. In this context, obtaining a modular structure for programs is by no means straightforward since the output of an entire program cannot in general be composed from the output of its components. To better understand the effects of disjunctive information on modularity we restrict the scope of analysis to the case of disjunctive logic programs (DLPs) subject to stable-model semantics. We define the notion of a DLP-function, where a well-defined input/output interface is provided, and establish a novel module theorem which indicates the compositionality of stable-model semantics for DLP-functions. The module theorem extends the well-known splitting-set theorem and enables the decomposition of DLP-functions given their strongly connected components based on positive dependencies induced by rules. In this setting, it is also possible to split shared disjunctive rules among components using a generalized shifting technique. The concept of modular equivalence is introduced for the mutual comparison of DLP-functions using a generalization of a translation-based verification method.

Abstract Equilibrium logic is an approach to non-monotonic reasoning that extends the stable-model and answer-set semantics for logic programs. In particular, it includes the general case of nested logic programs, where arbitrary Boolean combinations are permitted in heads and bodies of rules, as special kinds of theories. In this paper, we present polynomial reductions of the main reasoning tasks associated with equilibrium logic and nested logic programs into quantified propositional logic, an extension of classical propositional logic where quantifications over atomic formulas are permitted. Thus, quantified propositional logic is a fragment of second-order logic, and its formulas are usually referred to as quantified Boolean formulas (QBFs). We provide reductions not only for decision problems, but also for the central semantical concepts of equilibrium logic and nested logic programs. In particular, our encodings map a given decision problem into some QBF such that the latter is valid precisely in case the former holds. The basic tasks we deal with here are the consistency problem, brave reasoning and skeptical reasoning. Additionally, we also provide encodings for testing equivalence of theories or programs under different notions of equivalence, viz. ordinary, strong and uniform equivalence. For all considered reasoning tasks, we analyse their computational complexity and give strict complexity bounds. Hereby, our encodings yield upper bounds in a direct manner. Besides this useful feature, our approach has the following benefits: First, our encodings yield a uniform axiomatisation for a variety of problems in a common language. Second, extant solvers for QBFs can be used as back-end inference engines to realise implementations of the encoded task in a rapid prototyping manner. Third, our axiomatisations also allow us to straightforwardly relate equilibrium logic with circumscription.

We consider the problem of representing arbitrary preferences in causal reasoning and planning systems. In planning, a preference may be seen as a goal or constraint that is desirable, but not necessary, to satisfy. To begin, we define a very general query language for histories, or interleaved sequences of world states and actions. Based on this, we specify a second language in which preferences are defined. A single preference defines a binary relation on histories, indicating that one history is preferred to the other. From this, one can define global preference orderings on the set of histories, the maximal elements of which are the preferred histories. The approach is very general and flexible; thus it constitutes a ‘base’ language in terms of which higher-level preferences may be defined. To this end, we investigate two fundamental types of preferences that we call choice and temporal preferences. We consider concrete strategies for these types of preferences and encode them in terms of our framework. We suggest how to express aggregates in the approach, allowing, e.g. the expression of a preference for histories with lowest total action costs. Last, our approach can be used to express other approaches and so serves as a common framework in which such approaches can be expressed and compared. We illustrate this by indicating how an approach due to Son and Pontelli can be encoded in our approach, as well as the language PDDL3.

Abstract Through the Internet and the World-Wide Web, a vast number of information sources has become available, which offer information on various subjects by different providers, often in heterogeneous formats. This calls for tools and methods for building an advanced information-processing infrastructure. One issue in this area is the selection of suitable information sources in query answering. In this paper, we present a knowledge-based approach to this problem, in the setting where one among a set of information sources (prototypically, data repositories) should be selected for evaluating a user query. We use extended logic programs (ELPs) to represent rich descriptions of the information sources, an underlying domain theory, and user queries in a formal query language (here, XML-QL, but other languages can be handled as well). Moreover, we use ELPs for declarative query analysis and generation of a query description. Central to our approach are declarativesource-selection programs, for which we define syntax and semantics. Due to the structured nature of the considered data items, the semantics of such programs must carefully respect implicit context information in source-selection rules, and furthermore combine it with possible user preferences. A prototype implementation of our approach has been realized exploiting the DLV KR system and its PLP front-end for prioritized ELPs. We describe a representative example involving specific movie databases, and report about experimental results.

Towards providing a suitable tool for building the Rule Layer of the Semantic Web, hex -programs have been introduced as a special kind of logic programs featuring capabilities for higher-order reasoning, interfacing with external sources of computation, and default negation. Their semantics is based on the notion of answer sets, providing a transparent interoperability with the Ontology Layer of the Semantic Web and full declarativity. In this paper, we identify classes of hex -programs feasible for implementation yet keeping the desirable advantages of the full language. A general method for combining and evaluating sub-programs belonging to arbitrary classes is introduced, thus enlarging the variety of programs whose execution is practicable. Implementation activity on the current prototype is also reported. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

We present the system dlvhex, a solver for HEX-programs, which are nonmonotonic logic programs admitting both higher-order atoms as well as external atoms. Higher-order features are widely acknowledged as being useful for various tasks, including meta-reasoning. Furthermore, the possibility to exchange knowledge with external sources in a fully declarative paradigm such as answer-set programming (ASP) becomes increasingly important, in particular in view of applications in the semantic-Web area. Through external atoms, HEX-programs can deal with external knowledge and reasoners of various nature, such as RDF datasets or description-logics knowledge bases

The language of HEX-programs under the answer-set semantics is designed for interoperating with heterogeneous sources via external atoms and for meta-reasoning via higher-order literals in the context of the semantic Web. As an important technique in managing knowledge bases, the notion of forgetting has received increasing interest in the knowledge-representation area. In this paper, we introduce a semantics-based theory of forgetting for HEX-programs and, in turn, for a class of OWL/RDF(S) ontologies which allows to fully employ semantic information in managing ontologies like editing, merging, aligning, and redundancy removal

Recently, several approaches to updating knowledge bases modeled as extended logic programs have been introduced, ranging from basic methods to incorporate (sequences of) sets of rules into a logic program, to more elaborate methods which use an update policy for specifying how updates must be incorporated. In this article, we introduce a framework for reasoning about evolving knowledge bases, which are represented as extended logic programs and maintained by an update policy. We first describe a formal model which captures various update approaches, and we define a logical language for expressing properties of evolving knowledge bases. We then investigate semantical and computational properties of our framework, where we focus on properties of knowledge states with respect to the canonical reasoning task of whether a given formula holds in a given evolving knowledge base. In particular, we present finitary characterizations of the evolution for certain classes of framework instances, which can be exploited for obtaining decidability results. In more detail, we characterize the complexity of reasoning for some meaningful classes of evolving knowledge bases, ranging from polynomial to double exponential space complexity.

In recent years, there has been a large amount of disparate work concerning the representation and reasoning with qualitative preferential information by means of approaches to nonmonotonic reasoning. Given the variety of underlying systems, assumptions, motivations, and intuitions, it is difficult to compare or relate one approach with another. Here, we present an overview and classification for approaches to dealing with preference. A set of criteria for classifying approaches is given, followed by a set of desiderata that an approach might be expected to satisfy. A comprehensive set of approaches is subsequently given and classified with respect to these sets of underlying principles.

In this paper, we show how an approach to belief revision and belief contraction can be axiomatized by means of quantified Boolean formulas. Specifically, we consider the approach of belief change scenarios, a general framework that has been introduced for expressing different forms of belief change. The essential idea is that for a belief change scenario (K, R, C), the set of formulas K, representing the knowledge base, is modified so that the sets of formulas R and C are respectively true in, and consistent with the result. By restricting the form of a belief change scenario, one obtains specific belief change operators including belief revision, contraction, update, and merging. For both the general approach and for specific operators, we give a quantified Boolean formula such that satisfying truth assignments to the free variables correspond to belief change extensions in the original approach. Hence, we reduce the problem of determining the results of a belief change operation to that of satisfiability. This approach has several benefits. First, it furnishes an axiomatic specification of belief change with respect to belief change scenarios. This then leads to further insight into the belief change framework. Second, this axiomatization allows us to identify strict complexity bounds for the considered reasoning tasks. Third, we have implemented these different forms of belief change by means of existing solvers for quantified Boolean formulas. As well, it appears that this approach may be straightforwardly applied to other specific approaches to belief change.

We introduce a methodology and framework for expressing general preference information in logic programming under the answer set semantics. An ordered logic program is an extended logic program in which rules are named by unique terms, and in which preferences among rules are given by a set of atoms of form s [pr ] t where s and t are names. An ordered logic program is transformed into a second, regular, extended logic program wherein the preferences are respected, in that the answer sets obtained in the transformed program correspond with the preferred answer sets of the original program. Our approach allows the specification of dynamic orderings, in which preferences can appear arbitrarily within a program. Static orderings (in which preferences are external to a logic program) are a trivial restriction of the general dynamic case. First, we develop a specific approach to reasoning with preferences, wherein the preference ordering specifies the order in which rules are to be applied. We then demonstrate the wide range of applicability of our framework by showing how other approaches, among them that of Brewka and Eiter, can be captured within our framework. Since the result of each of these transformations is an extended logic program, we can make use of existing implementations, such as dlv and smodels. To this end, we have developed a publicly available compiler as a front-end for these programming systems.

In this paper, we consider an approach to update nonmonotonic knowledge bases represented as extended logic programs under the answer set semantics. In this approach, new information is incorporated into the current knowledge base subject to a causal rejection principle, which enforces that, in case of conflicts between rules, more recent rules are preferred and older rules are overridden. Such a rejection principle is also exploited in other approaches to update logic programs, notably in the method of dynamic logic programming, due to Alferes et al. One of the central issues of this paper is a thorough analysis of various properties of the current approach, in order to get a better understanding of the inherent causal rejection principle. For this purpose, we review postulates and principles for update and revision operators which have been proposed in the area of theory change and nonmonotonic reasoning. Moreover, some new properties for approaches to updating logic programs are considered as well. Like related update approaches, the current semantics does not incorporate a notion of minimality of change, so we consider refinements of the semantics in this direction. We also investigate the relationship of our approach to others in more detail. In particular, we show that the current approach is semantically equivalent to inheritance programs, which have been independently defined by Buccafurri et al., and that it coincides with certain classes of dynamic logic programs. In view of this analysis, most of our results about properties of the causal rejection principle apply to each of these approaches as well. Finally, we also deal with computational issues. Besides a discussion on the computational complexity of our approach, we outline how the update semantics and its refinements can be directly implemented on top of existing logic programming systems. In the present case, we implemented the update approach using the logic programming system DLV.

At present, the search for specific information on the World Wide Web is faced with several problems, which arise on the one hand from the vast number of information sources available, and on the other hand, from their intrinsic heterogeneity, since standards are missing. A promising approach for solving the complex problems emerging in this context is the use of multi-agent systems of information agents, which cooperatively solve advanced information-retrieval problems. This requires advanced capabilities to address complex tasks, such as search and assessment of information sources, query planning, information merging and fusion, dealing with incomplete information, and handling of inconsistency. In this paper, our interest lies in the role which some methods from the field of declarative logic programming can play in the realization of reasoning capabilities for information agents. In particular, we are interested to see how they can be used, extended, and further developed for the specific needs of this application domain. We review some existing systems and current projects, which typically address information-integration problems. We then focus on declarative knowledge-representation methods, and review and evaluate approaches and methods from logic programming and nonmonotonic reasoning for information agents. We discuss advantages and drawbacks, and point out the possible extensions and open issues.

It is well-known that almost all nonmonotonic formalisms have a higher worst-case complexity than classical reasoning. In some sense, this observation denies one of the original motivations of nonmonotonic systems, which was the expectation taht nonmonotonic rules should help to speed-up the reasoning process, and not make it more difficult. In this paper, we look at this issue from a proof-theoretical perspective. We consider analytic calculi for certain nonmonotonic logis and analyze to what extent the presence of nonmonotonic rules can simplify the search for proofs. In particular, we show that there are classes of first-order formulae which have only extremely long “classical” proofs, i.e., proofs without applications of nonmonotonic rules, but there are short proofs using nonmonotonic inferences. Hence,despite the increase of complexity in the worst case, there are instances where nonmonotonic reasoning can be much simpler than classical (cut-free) reasoning.