ABSTRACT. The belief revision literature only contains few approaches with a modal logic basis. This talk discusses how the Alchourron-Gärdenfors-Makinson (AGM) approach to belief revision can be extended from propositional logic to modal logic S5. We propose three new rationality postulates involving the modal operator of possibility $\Diamond$: 

(M1) If $\varphi \land \Diamond \mu$ is consistent, then $\varphi \ast \mu \vdash \Diamond \varphi$.           

(M2) If $\psi \land \Diamond \mu$ is consistent, then $\varphi \vdash \psi$ implies $\varphi \ast \Diamond \mu \vdash \psi$, for propositional $\mu$.           

(M3) If $\psi \land \Diamond \mu$ is consistent, then $\varphi \vdash \Diamond \psi$ implies $\varphi \ast \mu \vdash \Diamond \psi$, for propositional $\mu$.       

The associated distance semantics is in terms of a lexicographic ordering that lifts the Hamming distance from a distance between valuations to a distance between pointed S5 models. Based on this account, we revisit a consequence of the AGM approach that has been much debated in knowledge representation, namely that the revisions of $p \land q$ and $p \land (p \rightarrow q)$ should be identical. We show that the problem disappears if one replaces material implication $\varphi \rightarrow \psi$ by strict implication $\varphi \succ \psi$. The latter can be expressed in modal logic as the necessity of material implication, that is, as $\Box(\varphi \rightarrow \psi)$.   

The talk is based on joint work with Carlos Aguilera-Ventura and Jonathan Ben-Naim and is based on our paper ``Minimal Change in Modal Logic S5'' (Proc. AAAI 2025) and ongoing work.

ABSTRACT. Within the formal setting of the Lockean thesis, an agent belief set is defined in terms of degrees of confidence and these latter are described in probabilistic terms. This approach is of established interest, notwithstanding some limitations that makes its use troublesome in some contexts, like for instance in belief change theory. Precisely, Lockean belief sets are not generally closed under (classical) logical deduction.

The aim of the present paper is twofold: from one side we provide two characterizations of those belief sets that are closed under classical logic deduction, and from the other we propose an approach to probabilistic update that allows us for a minimal revision of those beliefs, i.e., a revision of a belief set obtained by making the fewest possible changes to the existing belief set while still accommodating the new information. In particular, we show how we can deductively close a belief set via a minimal revision.

ABSTRACT. State-of-the-art Answer Set Programming (ASP) systems that adopt the Ground&Solve approach are limited by the grounding bottleneck. This issue arises whenever the grounding produces a large propositional program that cannot be handled efficiently during solving. The grounding bottleneck can be mitigated through compilation-based ASP solving, which avoids generating propositional rules for selected ''problematic'' subprograms. However, compilation-based ASP systems generate in advance the propositional atoms required for solving the problem. As a consequence, as soon as a large number of propositional atoms is required, also this approach exhibits overhead. In this paper a novel compilation-based technique is presented that overcomes this limitation by discovering propositional atoms lazily, i.e., during the solving process. Empirical results confirm the effectiveness of the proposed approach.

ABSTRACT. Action reversibility in planning deals with the question whether the consequences of a given action can be undone so that the state of the environment returns to what it was before the action was applied. This problem is known to be PSPACE-complete in general. In this paper, we evaluate two PSPACE-complete logic programming languages, namely: Quantified Answer Set Programming (QASP) that extends Answer Set Programming (ASP) with quantified atoms; and Bule, a logic programming language that extends Quantified Boolean Formulas (QBFs) with Datalog-like rules in order to separate the problem domain and problem instance. We give two novel encodings for the problem of action reversibility and perform experiments to see how the solvers for these two languages compare to established methods.

ABSTRACT. In this paper, we survey literature on grounding in Answer Set Programming (ASP) and related fields, analyse the common benchmarks used for this purpose, and introduce a new grounding benchmark called DIRT. In ASP, reasoning engines typically rely on a ``ground-and-solve'' approach, in which a high-level description of a problem domain (e.g., an Answer Set Program) is first transformed into a low-level description (e.g., aspif) in order to solve. This process, better known as grounding, has a significant effect on the overall speed of the reasoning engine. For this reason, literature contains numerous works dedicated to optimizing various aspects of the grounding process. However, each paper tends to measure their improvements on distinct benchmarks, making a direct comparison between works often difficult. We argue that this is caused by a lack of standardized benchmarks for grounding, and substantiate this claim through a survey of grounding literature. Based on this survey, we have distilled the Dataset for Instantiating in Reasoning Tools~(DIRT) as a specialized grounding benchmark. We provide encodings for ASP and ASP-like formats, and present their baseline performance on this problem set. In this way, our benchmark suite can help identify bottlenecks in state-of-the-art grounders, and can serve as a standardized dataset for future works on grounding.

ABSTRACT. In answer set programming, a program verification task can be sometimes accomplished by transforming rules into first-order sentences so that the task is reduced to reasoning in classical logic, and invoking a resolution theorem prover. The proof assistant anthem, which implements this idea, allows us to reason about programs written in mini-gringo -- a subset of the input language of the grounder gringo. The goal of this paper is to extend the syntax of terms permitted in that subset. First, instead of the specific choice of arithmetic functions made in earlier publications on mini-gringo, we approach integer arithmetic in an abstract way, so that different choices are allowed for different dialects of the language. Second, symbolic constants can be used now as function symbols. This generalization preserves the main property of the more limited form of the language established in earlier work: mini-gringo rules can be faithfully represented by first-order sentences.

ABSTRACT. The proof assistant Anthem can be used to verify equivalence of logic programming solutions to the same problem that have been independently developed by different programmers.