检索结果-内蒙古大学图书馆

An iterative approach to precondition inference using constrained Horn clauses

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Kafle, Bishoksan Gallagher, John P. Gange, Graeme Schachte, Peter Søndergaard, Harald Stuckey, Peter J. University of Melbourne Roskilde University IMDEA Software Institute Monash University

We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assertions in the program are not violated. Constrained Horn clauses (CHCs) are used to model the program and assertions in a uniform way, and we use standard abstract interpretations to derive an over-approximation of the set of unsafe initial states. The precondition then is the constraint corresponding to the complement of that set, under-approximating the set of safe initial states. This idea of complementation is not new, but previous attempts to exploit it have suffered from loss of precision. Here we develop an iterative specialisation algorithm to give more precise, and in some cases optimal safety conditions. The algorithm combines existing transformations, namely constraint specialisation, partial evaluation and a trace elimination transformation. The last two of these transformations perform polyvariant specialisation, leading to disjunctive constraints which improve precision. The algorithm is implemented and tested on a benchmark suite of programs from the literature in precondition inference and software verification competitions. Under consideration for acceptance in TPLP. Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

Strong equivalence for epistemic logic programs made easy (extended version)

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Faber, Wolfgang Morak, Michael Woltran, Stefan Alpen-Adria-Universität Klagenfurt Klagenfurt Austria TU Wien Vienna Austria

Epistemic logic Programs (ELPs), that is, Answer Set programming (ASP) extended with epistemic operators, have received renewed interest in recent years, which led to a flurry of new research, as well as efficient solvers. An important question is under which conditions a sub-program can be replaced by another one without changing the meaning, in any context. This problem is known as strong equivalence, and is well-studied for ASP. For ELPs, this question has been approached by embedding them into epistemic extensions of equilibrium logics. In this paper, we consider a simpler, more direct characterization that is directly applicable to the language used in state-of-the-art ELP solvers. This also allows us to give tight complexity bounds, showing that strong equivalence for ELPs remains coNP-complete, as for ASP. We further use our results to provide syntactic characterizations for tautological rules and rule subsumption for ELPs. Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

An ASP methodology for understanding narratives about stereotypical activities

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Inclezan, Daniela Zhang, Qinglin Balduccini, Marcello Israney, Ankush Miami University OxfordOH45056 United States Saint Joseph's University PhiladelphiaPA19131 United States Drexel University PhiladelphiaPA19104 United States

We describe an application of Answer Set programming to the understanding of narratives about stereotypical activities, demonstrated via question answering. Substantial work in this direction was done by Erik Mueller, who modeled stereotypical activities as scripts. His systems were able to understand a good number of narratives, but could not process texts describing exceptional scenarios. We propose addressing this problem by using a theory of intentions developed by Blount, Gelfond, and Balduccini. We present a methodology in which we substitute scripts by activities (i.e., hierarchical plans associated with goals) and employ the concept of an intentional agent to reason about both normal and exceptional scenarios. We exemplify the application of this methodology by answering questions about a number of restaurant stories. This paper is under consideration for acceptance in TPLP. Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

Technical note the external interface for extending WASP

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Dodaro, Carmine Ricca, Francesco DIBRIS University of Genova Genova Italy DEMACS University of Calabria Rende Italy

Answer set programming (ASP) is a successful declarative formalism for knowledge representation and reasoning. The evaluation of ASP programs is nowadays based on the Conflict-Driven Clause Learning (CDCL) backtracking search algorithm. Recent work suggested that the performance of CDCL-based implementations can be considerably improved on specific benchmarks by extending their solving capabilities with custom heuristics and propagators. However, embedding such algorithms into existing systems requires expert knowledge of the internals of ASP implementations. The development of effective solver extensions can be made easier by providing suitable programming interfaces. In this paper, we present the interface for extending the CDCL-based ASP solver WASP. The interface is both general, i.e. it can be used for providing either new branching heuristics and propagators, and external, i.e. the implementation of new algorithms requires no internal modifications of WASP. Moreover, we review the applications of the interface witnessing it can be successfully used to extend WASP for solving effectively hard instances of both real-world and synthetic problems. Under consideration in Theory and Practice of logic programming (TPLP). Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Basold, Henning Komendantskaya, Ekaterina Li, Yue CNRS ENS Lyon France Heriot-Watt University United Kingdom

We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is cast in terms of coinductive uniform proofs;its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality;and soundness of both proof systems is proven relative to a novel coalgebraic description of complete Herbrand *** Codes 03B70 Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

Tree dimension in verification of constrained Horn clauses

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Kafle, Bishoksan Gallagher, John P. Ganty, Pierre University of Melbourne Roskilde University IMDEA Software Institute IMDEA Software Institute

In this paper we show how the notion of tree dimension can be used in the verifficationof constrained Horn clauses (CHCs). The dimension of a tree is a numerical measure of its branching complexity and the concept here applies to Horn clause derivation trees. Derivation trees of dimension zero correspond to derivations using linear CHCs, while trees of higher dimension arise from derivations using non-linear CHCs. We show how to instrument CHCs predicates with an extra argument for the dimension, allowing a CHC verifier to reason about bounds on the dimension of derivations. Given a set of CHCs P, we define a transformation of P yielding a dimension bounded set of CHCs P≤k. The set of derivations for P≤k consists of the derivations for P that have dimension at most k. We also show how to construct a set of clauses denoted P>k whose derivations have dimension exceeding *** then present algorithms using these constructions to decompose a CHC verification problem. One variation of this decomposition considers derivations of successively increasing dimension. The paper includes descriptions of implementations and experimental results. Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

Stratified negation in limit datalog programs

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Kaminski, Mark Grau, Bernardo Cuenca Kostylev, Egor V. Motik, Boris Horrocks, Ian Department of Computer Science University of Oxford United Kingdom

There has recently been an increasing interest in declarative data analysis, where analytic tasks are specified using a logical language, and their implementation and optimisation are delegated to a general-purpose query engine. Existing declarative languages for data analysis can be formalised as variants of logic programming equipped with arithmetic function symbols and/or aggregation, and are typically undecidable. In prior work, the language of limit programs was proposed, which is sufficiently powerful to capture many analysis tasks and has decidable entailment problem. Rules in this language, however, do not allow for negation. In this paper, we study an extension of limit programs with stratified negation-as-failure. We show that the additional expressive power makes reasoning computationally more demanding, and provide tight data complexity bounds. We also identify a fragment with tractable data complexity and sufficient expressivity to capture many relevant tasks. Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

Shared aggregate sets in answer set programming

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Alviano, Mario Dodaro, Carmine Maratea, Marco DEMACS University of Calabria Italy DIBRIS University of Genova Italy

Aggregates are among the most frequently used linguistic extensions of answer set programming. The result of an aggregation may introduce new constants during the instantiation of the input program, a feature known as value invention. When the aggregation involves literals whose truth value is undefined at instantiation time, modern grounders introduce several instances of the aggregate, one for each possible interpretation of the undefined literals. This paper introduces new data structures and techniques to handle such cases, and more in general aggregations on the same aggregate set identified in the ground program in input. The proposed solution reduces the memory footprint of the solver without sacrificing efficiency. On the contrary, the performance of the solver may improve thanks to the addition of some simple entailed clauses which are not easily discovered otherwise, and since redundant computation is avoided during propagation. Empirical evidence of the potential impact of the proposed solution is given. (Under consideration for acceptance in TPLP). Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming

Temporal answer set programming on finite traces

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Cabalar, Pedro Kaminski, Roland Schaub, Torsten Schuhmann, Anna University of Corunna Spain University of Potsdam Germany

In this paper, we introduce an alternative approach to Temporal Answer Set programming that relies on a variation of Temporal Equilibrium logic (TEL) for finite traces. This approach allows us to even out the expressiveness of TEL over infinite traces with the computational capacity of (incremental) Answer Set programming (ASP). Also, we argue that finite traces are more natural when reasoning about action and change. As a result, our approach is readily implementable via multi-shot ASP systems and benefits from an extension of ASP's full-fledged input language with temporal operators. This includes future as well as past operators whose combination offers a rich temporal modeling language. For computation, we identify the class of temporal logic programs and prove that it constitutes a normal form for our approach. Finally, we outline two implementations, a generic one and an extension of the ASP system clingo. Copyright © 2018, The Authors. All rights reserved.

关键词： logic programming