Answer Set programming with Quantifiers ASP(Q) is a recent extension of Answer Set programming (ASP) that allows one to model problems from the entire polynomial hierarchy. Earlier work focused on demonstrating modeli...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Answer Set programming with Quantifiers ASP(Q) is a recent extension of Answer Set programming (ASP) that allows one to model problems from the entire polynomial hierarchy. Earlier work focused on demonstrating modeling capabilities of ASP(Q). In this paper, we propose a modular ASP(Q) solver that translates a quantified ASP program together with a given data instance into a Quantified Boolean Formula (QBF) to be solved by any QBF solver. We evaluate the performance of our solver on several instances and with different back-end QBF solvers, demonstrating the efficacy of ASP(Q) as a tool for rapid modeling and solving of complex combinatorial problems. The benchmark problems we use include two new ones, Argumentation Coherence and Para-coherent ASP, for which we develop elegant ASP(Q) encodings.
Answer Set programming (ASP) is a well-established declarative AI formalism for knowledge representation and reasoning. ASP systems were successfully applied to both industrial and academic problems. Nonetheless, thei...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Answer Set programming (ASP) is a well-established declarative AI formalism for knowledge representation and reasoning. ASP systems were successfully applied to both industrial and academic problems. Nonetheless, their performance can be improved by embedding domain-specific heuristics into their solving process. However, the development of domain-specific heuristics often requires both a deep knowledge of the domain at hand and a good understanding of the fundamental working principles of the ASP solvers. In this paper, we investigate the use of deep learning techniques to automatically generate domain-specific heuristics for ASP solvers targeting the well-known graph coloring problem. Empirical results show that the idea is promising: the performance of the ASP solver WASP can be improved.
Answer set programming (ASP) solvers have advanced in recent years, with a variety of different specialisation and overall development. Thus, even more complex and detailed programs can be solved. A side effect of thi...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
Answer set programming (ASP) solvers have advanced in recent years, with a variety of different specialisation and overall development. Thus, even more complex and detailed programs can be solved. A side effect of this development are growing solution spaces and the problem of how to find those answer sets one is interested in. One general approach is to give an overview in form of a small number of highly diverse answer sets. By choosing a favourite and repeating the process, the user is able to leap through the solution space. But finding highly diverse answer sets is computationally expensive. In this paper we introduce a new approach called Tunas for Trade Up Navigation for Answer Sets to find diverse answer sets by reworking existing solution collections. The core idea is to collect diverse answer sets one after another by iteratively solving and updating the program. Once no more answer sets can be added to the collection, the program is allowed to trade answer sets from the collection for different answer sets, as long as the collection grows and stays diverse. Elaboration of the approach is possible in three variations, which we implemented and compared to established methods in an empirical evaluation. The evaluation shows that the Tunas approach is competitive with existing methods, and that efficiency of the approach is highly connected to the underlying logic program.
In this paper we develop a state transition function for partially observable multi-agent epistemic domains and implement it using Answer Set programming (ASP). The transition function computes the next state upon an ...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
In this paper we develop a state transition function for partially observable multi-agent epistemic domains and implement it using Answer Set programming (ASP). The transition function computes the next state upon an occurrence of a single action. Thus it can be used as a module in epistemic planners. Our transition function incorporates ontic, sensing and announcement actions and allows for arbitrary nested belief formulae and general common knowledge. A novel feature of our model is that upon an action occurrence, an observing agent corrects his (possibly wrong) initial beliefs about action precondition and his observability. By examples, we show that this step is necessary for robust state transition. We establish some properties of our state transition function regarding its soundness in updating beliefs of agents consistent with their observability.
Incorrectness logic (IL) has recently been advanced as a logical theory for compositionally proving the presence of bugs-dual to Hoare logic, which is used to compositionally prove their absence. Though IL was motivat...
详细信息
Incorrectness logic (IL) has recently been advanced as a logical theory for compositionally proving the presence of bugs-dual to Hoare logic, which is used to compositionally prove their absence. Though IL was motivated in large part by the aim of providing a logical foundation for bug-catching program analyses, it has remained an open question: is IL useful only retrospectively (to explain existing analyses), or can it actually be useful in developing new analyses which can catch real bugs in big programs? In this work, we develop Pulse-X, a new, automatic program analysis for catching memory errors, based on ISL, a recent synthesis of IL and separation logic. Using Pulse-X, we have found 15 new real bugs in OpenSSL, which we have reported to OpenSSL maintainers and have since been fixed. In order not to be overwhelmed with potential but false error reports, we develop a compositional bug-reporting criterion based on a distinction between latent and manifest errors, which references the under-approximate ISL abstractions computed by Pulse-X, and we investigate the fix rate resulting from application of this criterion. Finally, to probe the potential practicality of our bug-finding method, we conduct a comparison to Infer, a widely used analyzer which has proven useful in industrial engineering practice.
The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Pro...
ISBN:
(纸本)9783031911170
The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Programs;Constructive characterisations of the MUST-preorder for asynchrony;abstraction of memory block manipulations by symbolic loop folding;cognacy Queries over Dependence Graphs for Transparent Visualisations;an abstract, certified account of operational game semantics;artifact Report: an Abstract, Certified Account of Operational Game Semantics;neural Network Verification is a programming Language Challenge;stratified Type theory;coverage Semantics for Dependent Pattern Matching;variable Elimination as Rewriting in a Linear Lambda Calculus;a Program logic for Concurrent Randomized Programs in the Oblivious Adversary Model;iso-Recursive Multiparty Sessions and their Automated Verification;verifying Algorithmic Versions of the Lovász Local Lemma;Elucidating Type Conversions in SQL Engines.
The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Pro...
ISBN:
(纸本)9783031911200
The proceedings contain 32 papers. The special focus in this conference is on programming. The topics include: Formulas as Processes, Deadlock-Freedom as Choreographies;Sufficient Conditions for Robustness of RDMA Programs;Constructive characterisations of the MUST-preorder for asynchrony;abstraction of memory block manipulations by symbolic loop folding;cognacy Queries over Dependence Graphs for Transparent Visualisations;an abstract, certified account of operational game semantics;artifact Report: an Abstract, Certified Account of Operational Game Semantics;neural Network Verification is a programming Language Challenge;stratified Type theory;coverage Semantics for Dependent Pattern Matching;variable Elimination as Rewriting in a Linear Lambda Calculus;a Program logic for Concurrent Randomized Programs in the Oblivious Adversary Model;iso-Recursive Multiparty Sessions and their Automated Verification;verifying Algorithmic Versions of the Lovász Local Lemma;Elucidating Type Conversions in SQL Engines.
Processing programs as data is one of the successes of functional and logicprogramming. Higher-order functions, as program-processing programs are called in functional programming, and meta-programs, as they are call...
详细信息
Processing programs as data is one of the successes of functional and logicprogramming. Higher-order functions, as program-processing programs are called in functional programming, and meta-programs, as they are called in logicprogramming, are widespread declarative programming techniques. In logicprogramming, there is a gap between the meta-programmingpractice and its theory: The formalizations of meta-programming do not explicitly address its impredicativity and are not fully adequate. This article aims at overcoming this unsatisfactory situation by discussing the relevance of impredicativity to meta-programming, by revisiting former formalizations of meta-programming, and by defining Reflective Predicate logic, a conservative extension of first-order logic, which provides a simple formalization of meta-programming.
A Abstract dialectical frameworks (ADFs) are a well-studied generalisation of the prominent argumentation frameworks due to Phan Minh Dung. In this paper we propose to use reduced ordered binary decision diagrams (RoB...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
A Abstract dialectical frameworks (ADFs) are a well-studied generalisation of the prominent argumentation frameworks due to Phan Minh Dung. In this paper we propose to use reduced ordered binary decision diagrams (RoBDDs) as a suitable representation of the acceptance conditions of arguments within ADFs. We first show that computational complexity of reasoning on ADFs represented by RoBDDs is milder than in the general case, with a drop of one level in the polynomial hierarchy. Furthermore, we present a framework to systematically define heuristics for search space exploitation, based on easily retrievable properties of RoBDDs and the recently proposed approach of weighted faceted navigation for answer set programming. Finally, we present preliminary experiments of an implementation of our approach showing promise both when compared to state-of-the-art solvers and when developing heuristics for reasoning.
暂无评论