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.

We present plingo, an extension of the answer set programming (ASP) system clingo that incorporates various probabilistic reasoning modes. Plingo is based on $\textit{Lpmln}^{\pm }$, a simple variant of the probabilistic language Lpmln, which follows a weighted scheme derived from Markov logic. This choice is motivated by the fact that the main probabilistic reasoning modes can be mapped onto enumeration and optimization problems and that $\textit{Lpmln}^{\pm }$ may serve as a middle-ground formalism connecting to other probabilistic approaches. Plingo offers three alternative frontends, for Lpmln, P-log, and ProbLog. These input languages and reasoning modes are implemented by means of clingo’s multi-shot and theory-solving capabilities. In this way, the core of plingo is an implementation of $\textit{Lpmln}^{\pm }$ in terms of modern ASP technology. On top of that, plingo implements a new approximation technique based on a recent method for answer set enumeration in the order of optimality. Additionally, in this work, we introduce a novel translation from $\textit{Lpmln}^{\pm }$ to ProbLog. This leads to a new solving method in plingo where the input program is translated and a ProbLog solver is executed. Our empirical evaluation shows that the different solving approaches of plingo are complementary and that plingo performs similarly to other probabilistic reasoning systems.

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.

Catamorphisms are functions that are recursively defined on list and trees and, in general, on algebraic data types (ADTs), and are often used to compute suitable abstractions of programs that manipulate ADTs. Examples of catamorphisms include functions that compute size of lists, orderedness of lists, and height of trees. It is well known that program properties specified through catamorphisms can be proved by showing the satisfiability of suitable sets of constrained Horn clauses (CHCs). We address the problem of checking the satisfiability of those sets of CHCs, and we propose a method for transforming sets of CHCs into equisatisfiable sets where catamorphisms are no longer present. As a consequence, clauses with catamorphisms can be handled without extending the satisfiability algorithms used by existing CHC solvers. Through an experimental evaluation on a nontrivial benchmark consisting of many list and tree processing algorithms expressed as sets of CHCs, we show that our technique is indeed effective and significantly enhances the performance of state-of-the-art CHC solvers.

DatalogMTL is an extension of Datalog with metric temporal operators that has found an increasing number of applications in recent years. Reasoning in DatalogMTL is, however, of high computational complexity, which makes reasoning in modern data-intensive applications challenging. In this paper we present a practical reasoning algorithm for the full DatalogMTL language, which we have implemented in a system called MeTeoR. Our approach effectively combines an optimised (but generally non-terminating) materialisation (a.k.a. forward chaining) procedure, which provides scalable behaviour, with an automata-based component that guarantees termination and completeness. To ensure favourable scalability of the materialisation component, we propose a novel seminaïve materialisation procedure for DatalogMTL enjoying the non-repetition property, which ensures that each rule instance will be applied at most once throughout its entire execution. Moreover, our materialisation procedure is enhanced with additional optimisations which further reduce the number of redundant computations performed during materialisation by disregarding rules as soon as it is certain that they cannot derive new facts in subsequent materialisation steps. Our extensive evaluation supports the practicality of our approach.