One of the differences among the various approaches to suspension-based tabled evaluation is the scheduling strategy. The two most popular strategies are local and batched evaluation. The former collects all the solut...
详细信息
One of the differences among the various approaches to suspension-based tabled evaluation is the scheduling strategy. The two most popular strategies are local and batched evaluation. The former collects all the solutions to a tabled predicate before making any one of them available outside the tabled computation. The latter returns answers one by one before computing them all, which in principle is better if only one answer (or a subset of the answers) is desired. Batched evaluation is closer to SLD evaluation in that it computes solutions lazily as they are demanded, but it may need arbitrarily more memory than local evaluation, which is able to reclaim memory sooner. Some programs which in practice can be executed under the local strategy quickly run out of memory under batched evaluation. This has led to the general adoption of local evaluation at the expense of the more depth-first batched strategy. In this paper we study the reasons for the high memory consumption of batched evaluation and propose a new scheduling strategy which we have termed swapping evaluation. Swapping evaluation also returns answers one by one before completing a tabled call, but its memory usage can be orders of magnitude less than batched evaluation. An experimental implementation in the XSB system shows that swapping evaluation is a feasible memory-scalable strategy that need not compromise execution speed.
An approach to the revision of logic programs under the answer set semantics is presented. For programs P and Q, the goal is to determine the answer sets that correspond to the revision of P by Q, denoted P * Q. A fun...
详细信息
An approach to the revision of logic programs under the answer set semantics is presented. For programs P and Q, the goal is to determine the answer sets that correspond to the revision of P by Q, denoted P * Q. A fundamental principle of classical (AGM) revision, and the one that guides the approach here, is the success postulate. In AGM revision, this stipulates that alpha is an element of K * alpha. By analogy with the success postulate, for programs P and Q, this means that the answer sets of Q will in some sense be contained in those of P * Q. The essential idea is that for P * Q, a three-valued answer set for Q, consisting of positive and negative literals, is first determined. The positive literals constitute a regular answer set, while the negated literals make up a minimal set of naf literals required to produce the answer set from Q. These literals are propagated to the program P, along with those rules of Q that are not decided by these literals. The approach differs from work in update logic programs in two main respects. First, we ensure that the revising logic program has higher priority, and so we satisfy the success postulate;second, for the preference implicit in a revision P * Q, the program Q as a whole takes precedence over P, unlike update logic programs, since answer sets of Q are propagated to P. We show that a core group of the AGM postulates are satisfied, as are the postulates that have been proposed for update logic programs.
We study the decidability of termination for two CH R dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity > 0). Both languages a...
详细信息
We study the decidability of termination for two CH R dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity > 0). Both languages allow the use of the = built-in in the body of rules, thus are built on a host language that supports unification. However each imposes one further restriction. The first CHR dialect allows only range-restricted rules, that is, it does not allow the use of variables in the body or in the guard of a rule if they do not appear in the head. We show that the existence of an infinite computation is decidable for this dialect. The second dialect instead limits the number of atoms in the head of rules to one. We prove that in this case, the existence of a terminating computation is decidable. These results show that both dialects are strictly less expressive(1) than Turing Machines. It is worth noting that the language (without function symbols) without these restrictions is as expressive as Turing Machines.
In this paper we explore the use of Answer Set programming (ASP) to formalize, and reason about, psychological knowledge. In the field of psychology, a considerable amount of knowledge is still expressed using only na...
详细信息
In this paper we explore the use of Answer Set programming (ASP) to formalize, and reason about, psychological knowledge. In the field of psychology, a considerable amount of knowledge is still expressed using only natural language. This lack of a formalization complicates accurate studies, comparisons, and verification of theories. We believe that ASP, a knowledge representation formalism allowing for concise and simple representation of defaults, uncertainty, and evolving domains, can be used successfully for the formalization of psychological knowledge. To demonstrate the viability of ASP for this task, in this paper we develop an ASP-based formalization of the mechanics of Short-Term Memory. We also show that our approach can have rather immediate practical uses by demonstrating an application of our formalization to the task of predicting a user's interaction with a graphical interface.
This paper develops automated testing and debugging techniques for answer set solver development. We describe a flexible grammar-based black-box ASP fuzz testing tool which is able to reveal various defects such as un...
详细信息
This paper develops automated testing and debugging techniques for answer set solver development. We describe a flexible grammar-based black-box ASP fuzz testing tool which is able to reveal various defects such as unsound and incomplete behavior, i.e. invalid answer sets and inability to find existing solutions, in state-of-the-art answer set solver implementations. Moreover, we develop delta debugging techniques for shrinking failure-inducing inputs on which solvers exhibit defective behavior. In particular, we develop a delta debugging algorithm in the context of answer set solving, and evaluate two different elimination strategies for the algorithm.
ML5 is a programming language for spatially distributed computing, based on a Curry-Howard correspondence with the modal logic S5. However, the ML5 programming language differs from the logic in several ways. In this ...
详细信息
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 for debugging an answer-set progr...
详细信息
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 for debugging an 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.
The theory BV of bit-vectors, i.e. fixed-size arrays of bits equipped with standard low-level machine instructions, is becoming very popular in formal verification. Standard solvers for this theory are based on a bit-...
详细信息
ISBN:
(纸本)9783642120015
The theory BV of bit-vectors, i.e. fixed-size arrays of bits equipped with standard low-level machine instructions, is becoming very popular in formal verification. Standard solvers for this theory are based on a bit-level encoding into propositional logic and SAT-based resolution techniques. In this paper, we investigate an alternative approach based on a word-level encoding into bounded arithmetic and Constraint logicprogramming (CLP) resolution techniques. We define an original CLP framework (domains and propagators) dedicated to bit-vector constraints. This framework is implemented in a prototype and thorough experimental studies have been conducted. The new approach is shown to perform much better than standard CLP-based approaches, and to considerably reduce the gap with the best SAT-based BV solvers.
The need for integration of ontologies with nonmonotonic rules has been gaining importance in a number of areas, such as the Semantic Web. A number of researchers addressed this problem by proposing a unified semantic...
详细信息
The need for integration of ontologies with nonmonotonic rules has been gaining importance in a number of areas, such as the Semantic Web. A number of researchers addressed this problem by proposing a unified semantics for hybrid knowledge bases composed of both an ontology (expressed in a fragment of first-order logic) and nonmonotonic rules. These semantics have matured over the years, but only provide solutions for the static case when knowledge does not need to evolve. In this paper we take a first step towards addressing the dynamics of hybrid knowledge bases. We focus on knowledge updates and, considering the state of the art of belief update, ontology update and rule update, we show that current solutions are only partial and difficult to combine. Then we extend the existing work on ABox updates with rules, provide a semantics for such evolving hybrid knowledge bases and study its basic properties. To the best of our knowledge, this is the first time that an update operator is proposed for hybrid knowledge bases.
Testing is a vital part of the software development process. Test Case Generation (TCG) is the process of automatically generating a collection of test-cases which are applied to a system under test. White-box TCG is ...
详细信息
Testing is a vital part of the software development process. Test Case Generation (TCG) is the process of automatically generating a collection of test-cases which are applied to a system under test. White-box TCG is usually performed by means of symbolic execution, i.e., instead of executing the program on normal values (e.g., numbers), the program is executed on symbolic values representing arbitrary values. When dealing with an object-oriented (OO) imperative language, symbolic execution becomes challenging as, among other things, it must be able to backtrack, complex heap-allocated data structures should be created during the TCG process and features like inheritance, virtual invocations and exceptions have to be taken into account. Due to its inherent symbolic execution mechanism, we pursue in this paper that Constraint logicprogramming (CLP) has a promising application field in TCG. We will support our claim by developing a fully CLP-based framework to TCG of an OO imperative language, and by assessing it on a corresponding implementation on a set of challenging Java programs.
暂无评论