Solving a decision theory problem usually involves finding the actions, among a set of possible ones, which optimize the expected reward, while possibly accounting for the uncertainty of the environment. In this paper...
详细信息
Solving a decision theory problem usually involves finding the actions, among a set of possible ones, which optimize the expected reward, while possibly accounting for the uncertainty of the environment. In this paper, we introduce the possibility to encode decision theory problems with Probabilistic Answer Set programming under the credal semantics via decision atoms and utility attributes. To solve the task, we propose an algorithm based on three layers of Algebraic Model Counting, that we test on several synthetic datasets against an algorithm that adopts answer set enumeration. Empirical results show that our algorithm can manage non-trivial instances of programs in a reasonable amount of time.
Advances in incremental Datalog evaluation strategies have made Datalog popular among use cases with constantly evolving inputs such as static analysis in continuous integration and deployment pipelines. As a result, ...
详细信息
Advances in incremental Datalog evaluation strategies have made Datalog popular among use cases with constantly evolving inputs such as static analysis in continuous integration and deployment pipelines. As a result, new logicprogramming debugging techniques are needed to support these emerging use *** paper introduces an incremental debugging technique for Datalog, which determines the failing changes for a rollback in an incremental setup. Our debugging technique leverages a novel incremental provenance method. We have implemented our technique using an incremental version of the Souffl & eacute;Datalog engine and evaluated its effectiveness on the DaCapo Java program benchmarks analyzed by the Doop static analysis library. Compared to state-of-the-art techniques, we can localize faults and suggest rollbacks with an overall speedup of over 26.9 $\times$ while providing higher quality results.
Probabilistic Answer Set programming under the credal semantics extends Answer Set programming with probabilistic facts that represent uncertain information. The probabilistic facts are discrete with Bernoulli distrib...
详细信息
Probabilistic Answer Set programming under the credal semantics extends Answer Set programming with probabilistic facts that represent uncertain information. The probabilistic facts are discrete with Bernoulli distributions. However, several real-world scenarios require a combination of both discrete and continuous random variables. In this paper, we extend the PASP framework to support continuous random variables and propose Hybrid Probabilistic Answer Set programming. Moreover, we discuss, implement, and assess the performance of two exact algorithms based on projected answer set enumeration and knowledge compilation and two approximate algorithms based on sampling. Empirical results, also in line with known theoretical results, show that exact inference is feasible only for small instances, but knowledge compilation has a huge positive impact on performance. Sampling allows handling larger instances but sometimes requires an increasing amount of memory.
Answer set programming (ASP), a well-known declarative logicprogramming paradigm, has recently found practical application in Process Mining. In particular, ASP has been used to model tasks involving declarative spec...
详细信息
Answer set programming (ASP), a well-known declarative logicprogramming paradigm, has recently found practical application in Process Mining. In particular, ASP has been used to model tasks involving declarative specifications of business processes. In this area, Declare stands out as the most widely adopted declarative process modeling language, offering a means to model processes through sets of constraints valid traces must satisfy, that can be expressed in linear temporal logic over finite traces (LTL$_{\text {f}}$). Existing ASP-based solutions encode Declare constraints by modeling the corresponding LTL$_{\text {f}}$ formula or its equivalent automaton which can be obtained using established techniques. In this paper, we introduce a novel encoding for Declare constraints that directly models their semantics as ASP rules, eliminating the need for intermediate representations. We assess the effectiveness of this novel approach on two Process Mining tasks by comparing it with alternative ASP encodings and a Python library for Declare.
The representation of a temporal problem in answer set programming (ASP) usually boils down to using copies of variables and constraints, one for each time stamp, no matter whether it is directly encoded or expressed ...
详细信息
The representation of a temporal problem in answer set programming (ASP) usually boils down to using copies of variables and constraints, one for each time stamp, no matter whether it is directly encoded or expressed via an action or temporal language. The multiplication of variables and constraints is commonly done during grounding, and the solver is completely ignorant about the temporal relationship among the different instances. On the other hand, a key factor in the performance of today's ASP solvers is conflict-driven constraint learning. Our question in this paper is whether a constraint learned for particular time steps can be generalized and reused at other time steps, and ultimately whether this enhances the overall solver performance on temporal problems. Knowing well the domain of time, we study conditions under which learned dynamic constraints can be generalized. Notably, we identify a property of temporal representations that enables the generalization of learned constraints across all time steps. It turns out that most ASP planning encodings either satisfy this property or can be easily adapted to do so. In addition, we propose a general translation that transforms programs to fulfill this property. Finally, we empirically evaluate the impact of adding the generalized constraints to an ASP solver.
Linear logic gives us additive pairs in the form of the additive conjunction. Intuitionistic type theory gives us dependent pairs in the form of the dependent sum type. What happens when we combine these two kinds of ...
详细信息
ISBN:
(纸本)9783031745577;9783031745584
Linear logic gives us additive pairs in the form of the additive conjunction. Intuitionistic type theory gives us dependent pairs in the form of the dependent sum type. What happens when we combine these two kinds of pairs together? And is this new pair type useful in practice? To answer these questions, we employ quantitative type theory, which can describe both substructural and dependent types simultaneously. In our previous work, we introduced dependent additive pairs. In this work, we show how these pairs can be used in three completely different scenarios: folding data structures using linear recursion schemes, computing resource-aware proofs, and defining additive versions of inductive and coinductive types. Each of these scenarios is then illustrated by an implementation in the Janus language.
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.
The issue of fairness is a well-known challenge in Machine Learning (ML) that has gained increased importance with the emergence of Large Language Models (LLMs) and generative AI. Algorithmic bias can manifest during ...
详细信息
暂无评论