An Algebra of Causal Chains

TL;DR

This paper introduces an algebraic framework for causal logic programs that associates justifications with true atoms, enabling analysis of causes, redundancies, and relevance through algebraic and lattice-based methods.

Contribution

It presents a novel algebra of truth values for causal logic programs, linking proof trees to algebraic semantics and defining causal stable models.

Findings

Established a one-to-one correspondence between proof trees and algebraic interpretations.

Defined an algebra with addition, product, and concatenation operations for justifications.

Proved properties of the semantics, including fixpoint computation and causal stable models.

Abstract

In this work we propose a multi-valued extension of logic programs under the stable models semantics where each true atom in a model is associated with a set of justifications, in a similar spirit than a set of proof trees. The main contribution of this paper is that we capture justifications into an algebra of truth values with three internal operations: an addition '+' representing alternative justifications for a formula, a commutative product '*' representing joint interaction of causes and a non-commutative product '.' acting as a concatenation or proof constructor. Using this multi-valued semantics, we obtain a one-to-one correspondence between the syntactic proof tree of a standard (non-causal) logic program and the interpretation of each true atom in a model. Furthermore, thanks to this algebraic characterization we can detect semantic properties like redundancy and relevance of the obtained justifications. We also identify a lattice-based characterization of this algebra, defining a direct consequences operator, proving its continuity and that its least fix point can be computed after a finite number of iterations. Finally, we define the concept of causal stable model by introducing an analogous transformation to Gelfond and Lifschitz's program reduct.