The s-semantics makes it possible to explicitly deal with variables in program answers. So it seems suitable for programs using nonground data structures, like open lists. However it is difficult to find published exa...
详细信息
ISBN:
(数字)9783030988692
ISBN:
(纸本)9783030988692;9783030988685
The s-semantics makes it possible to explicitly deal with variables in program answers. So it seems suitable for programs using nonground data structures, like open lists. However it is difficult to find published examples of using the s-semantics to reason about particular programs. Here we apply s-semantics to prove correctness and completeness of Fruhwirth's n queens program. This is compared with a proof, published elsewhere, based on the standard semantics and Herbrand interpretations.
Extending the popular Answer Set programming (ASP) paradigm by introspective reasoning capacities has received increasing interest within the last years. Particular attention is given to the formalism of epistemic log...
详细信息
ISBN:
(纸本)9781956792003
Extending the popular Answer Set programming (ASP) paradigm by introspective reasoning capacities has received increasing interest within the last years. Particular attention is given to the formalism of epistemic logic programs (ELPs) where standard rules are equipped with modal operators which allow to express conditions on literals for being known or possible, i.e., contained in all or some answer sets, respectively. ELPs thus deliver multiple collections of answer sets, known as world views. Employing ELPs for reasoning problems so far has mainly been restricted to standard decision problems (complexity analysis) and enumeration (development of systems) of world views. In this paper, we first establish quantitative reasoning for ELPs, where the acceptance of a certain set of literals depends on the number (proportion) of world views that are compatible with the set. Second, we present a novel system capable of efficiently solving the underlying counting problems required for quantitative reasoning. Our system exploits the graph-based measure treewidth by iteratively finding (graph) abstractions of ELPs.
While there has been much cross-fertilization between functional and logic programming-e.g., leading to functional models of many Prolog features-this appears to be much less the case regarding probabilistic programmi...
详细信息
ISBN:
(数字)9783030994617
ISBN:
(纸本)9783030994600;9783030994617
While there has been much cross-fertilization between functional and logic programming-e.g., leading to functional models of many Prolog features-this appears to be much less the case regarding probabilistic programming, even though this is an area of mutual interest. Whereas functional programming often focuses on modeling probabilistic processes, logic programming typically focuses on modeling possible worlds. These worlds are made up of facts that each carry a probability and together give rise to a distribution semantics. The latter approach appears to be little-known in the functional programming community. This paper aims to remedy this situation by presenting a functional account of the distribution semantics of probabilistic logic programming that is based on possible worlds. We present a term monad for the monadic syntax of queries together with a natural interpretation in terms of boolean algebras. Then we explain that, because probabilities do not form a boolean algebra, they-and other interpretations in terms of commutative semirings-can only be computed after query normalisation to deterministic, decomposable negation normal form (d-DNNF). While computing the possible worlds readily gives such a normal form, it suffers from exponential blow-up. Using heuristic algorithms yields much better results in practice.
In temporal extensions of Answer Set programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts aw...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
In temporal extensions of Answer Set programming (ASP) based on linear-time, the behavior of dynamic systems is captured by sequences of states. While this representation reflects their relative order, it abstracts away the specific times associated with each state. In many applications, however, timing constraints are important like, for instance, when planning and scheduling go hand in hand. We address this by developing a metric extension of linear-time temporal equilibrium logic, in which temporal operators are constrained by intervals over natural numbers. The resulting Metric Equilibrium logic provides the foundation of an ASP-based approach for specifying qualitative and quantitative dynamic constraints. To this end, we define a translation of metric formulas into monadic first-order formulas and give a correspondence between their models in Metric Equilibrium logic and Monadic Quantified Equilibrium logic, respectively. Interestingly, our translation provides a blue print for implementation in terms of ASP modulo difference constraints.
CHC-COMP 2022 is the fifth edition of the competition of solvers for Constrained Horn Clauses. The competition was run in March 2022;the results were presented at the 9th Workshop on Horn Clauses for Verification and ...
详细信息
CHC-COMP 2022 is the fifth edition of the competition of solvers for Constrained Horn Clauses. The competition was run in March 2022;the results were presented at the 9th Workshop on Horn Clauses for Verification and Synthesis held in Munich, Germany, on April 3, 2022. This edition featured six solvers, and eight tracks consisting of sets of linear and nonlinear clauses with constraints over linear integer arithmetic, linear real arithmetic, arrays, and algebraic data types. This report provides an overview of the organization behind the competition runs: it includes the technical details of the competition setup as well as presenting the results of the 2022 edition.
This paper presents a new framework for generating test-case scenarios for autonomous vehicles. We address two challenges in automatic test-case generation: first, a formal notion of test-case complexity, and second, ...
详细信息
ISBN:
(纸本)9781665409674
This paper presents a new framework for generating test-case scenarios for autonomous vehicles. We address two challenges in automatic test-case generation: first, a formal notion of test-case complexity, and second, an algorithm to generate more-complex test-cases. We characterize the complexity of a test-case by its set of solutions, and compare two complexities by the subset relation. The novelty of our definition is that it only relies on the pass-fail criteria of the test-case, rather than indirect or subjective assessments of what may challenge an ego vehicle to pass a test-case. Given a testcase, we model the problem of generating a more complex test-case as a constraint-satisfaction search problem. The search variables are the changes to the given test-case, and the search constraints define a solution to the search problem. The constraints include steering geometry of cars, the geometry of lanes, the shape of cars, traffic rules, bounds on longitudinal acceleration of cars, etc. To conquer the computational challenge, we divide the constraints to three categories and satisfy them with simulation, answer set programming, and SMT solving. We have implemented our algorithm using the Scenic libraries and the CARLA simulator and generate test-cases for several 3-way and 4-way intersections with different topologies. Our experiments demonstrate that both CARLA's autopilot and autopilot-plus-RSS (Responsibility-Sensitive Safety) can fail as the complexity of test-cases increase.
The Model Reconciliation Problem (MRP) was introduced to address issues in explainable AI planning. A solution to a MRP is an explanation for the differences between the models of the human and the planning agent (rob...
详细信息
The Model Reconciliation Problem (MRP) was introduced to address issues in explainable AI planning. A solution to a MRP is an explanation for the differences between the models of the human and the planning agent (robot). Most approaches to solving MRPs assume that the robot, who needs to provide explanations, knows the human model. This assumption is not always realistic in several situations (e.g., the human might decide to update her model and the robot is unaware of the updates).In this paper, we propose a dialog-based approach for computing explanations of MRPs under the assumptions that (i) the robot does not know the human model;(ii) the human and the robot share the set of predicates of the planning domain and their exchanges are about action descriptions and fluents' values;(iii) communication between the parties is perfect;and (iv) the parties are truthful. A solution of a MRP is computed through a dialog, defined as a sequence of rounds of exchanges, between the robot and the human. In each round, the robot sends a potential explanation, called proposal, to the human who replies with her evaluation of the proposal, called response. We develop algorithms for computing proposals by the robot and responses by the human and implement these algorithms in a system that combines imperative means with answer set programming using the multi-shot feature of clingo.
Building reliable software is challenging because today's software supply chains are built and secured from tools and individuals from a broad range of organizations with complex trust relationships. In this setti...
详细信息
ISBN:
(纸本)9781450398855
Building reliable software is challenging because today's software supply chains are built and secured from tools and individuals from a broad range of organizations with complex trust relationships. In this setting, tracking the origin of each piece of software and understanding the security and privacy implications of using it is essential. In this work we aim to secure software supply chains by using verifiable policies in which the origin of information and the trust assumptions are first-order concerns and abusive evidence is discoverable. To do so, we propose Policy Transparency, a new paradigm in which policies are based on authorization logic and all claims issued in this policy language are made transparent by inclusion in a transparency log. Achieving this goal in a real-world setting is non-trivial and to do so we propose a novel software architecture called PolyLog. We find that this combination of authorization logic and transparency logs is mutually beneficial - transparency logs allow authorization logic claims to be widely available aiding in discovery of abuse, and making claims interpretable with policies allows misbehavior captured in the transparency logs to be handled proactively.
This article presents a review of Majority-Inverter Graphs (MIGs) and their practical use in various applications within logic synthesis. MIGs are directed acyclic graphs consisting of three-input majority nodes and r...
详细信息
This article presents a review of Majority-Inverter Graphs (MIGs) and their practical use in various applications within logic synthesis. MIGs are directed acyclic graphs consisting of three-input majority nodes and regular/complemented edges. They represent a paradigm shift in representing and optimizing logic using only majority (MAJ) and inversion (INV) functions. In this article, we review different optimization algorithms that work on MIGs, including algebraic, Boolean, and exact methods. We also describe different applications of MIGs in logic synthesis: From classical CMOS-based synthesis to their use for theoretical results and emerging technologies.
In this paper, we present a system, called xASP, for generating explanations that explain why an atom belongs to (or does not belong to) an answer set of a given program. The system can generate all possible explanati...
详细信息
ISBN:
(纸本)9783031157073;9783031157066
In this paper, we present a system, called xASP, for generating explanations that explain why an atom belongs to (or does not belong to) an answer set of a given program. The system can generate all possible explanations for a query without the need to simplify the program before computing explanations, i.e., it works with non-ground programs. These properties distinguish xASP from existing systems such as xClingo, DiscASP, exp(ASP(c)), and s(CASP), which also generate explanations for queries to logic programs under the answer set semantics but simplify and ground the programs (the three systems xClingo, DiscASP, exp(ASP(c))) or do not always generate all possible explanations (the system s(CASP)). In addition, the output of xASP is insensitive to syntactic variations such as the order conditions and the order of rules, which is also different from the output of s(CASP).
暂无评论