ABSTRACT. We introduce the Causal Transition Calculus (CTC), a multi-layered framework that integrates intervention-based reasoning, process algebra and modal logic to characterise actual causality in concurrent systems. We show that CTC is sound and complete for the modified Halpern&Pearl notion of causality, providing a correspondence between causal reasoning over process-algebraic models and their induced labelled transition systems. This new framework for causality is work in progress.

ABSTRACT. Causal reasoning is central in many applications, but mechanized support for it in expressive logical environments remains limited. We present a shallow semantical embedding of recursive causal models in classical Higher-Order Logic (HOL) and a corresponding Isabelle/HOL implementation within the \logikey\ framework. The embedding represents causal formulas as HOL predicates over families of structural equations, interventions as updates of these families in HOL, and solutions of recursive models through a constructive solver based on a topological order over endogenous variables. This yields direct mechanized support for the language of causality with interventions. We validate the embedding by mechanically verifying the axioms of the language. The work extends \logikey\ with mechanized support for causal models and illustrates how HOL can be used to rapidly prototype logics together with reusable theorem proving and model finding support.

ABSTRACT. The philosophical analysis of actual causation has relied on neuron diagrams (NDs) and structural causal models (SCMs). Both have helped sharpen the concept, but they only represent the end states rather than the dynamic development of the system, and theories of causation often employ unlawful counterfactuals, requiring ad hoc repairs like normality orderings. We introduce models from the field of concurrency theory, a field that deals with dynamic processes. NDs are translated into labeled transition systems with histories and independence relations. The resulting model supports a temporal logic with backtracking modalities, reordering of independent events, and causal modalities. We define several formulae that capture different notions of causation and apply them to standard vignettes (preemption, conjunction, trumping, double prevention). Unlike most approaches, the analysis remains within lawful states.

ABSTRACT. We ask the question: given a rule, like `Do Not Walk on the Grass', how can we figure out when it's OK to relax it? This can be thought of as figuring out the \textit{reason} for the rule, with the rule itself being just a particular application of this reason to a given context. For instance, the reason for `Do Not Walk on the Grass' is that `The grass should be preserved for everyone to enjoy'. Figuring out the reason allows us then to properly decide whether it is OK to modify the rule or relax in a given context. We offer a formalization of this analysis in the language of counter-factual programming. Since our behavior (and intentional behavior in general) is caused by our reasons and not just by mechanical causes, this can be seen as a formalization of Aristotle's teleological cause. Elucidating reasons for behavioral rules could be combined with more classical mechanical causality analysis to yield better designs of artificially intelligent agents.

ABSTRACT. We discuss two influential views of unification: mutual information unification (MIU) and common origin unification (COU). We propose a simple probabilistic measure for COU and compare it with Myrvold's (2003, 2007) probabilistic measure for MIU. We then explore how well these two measures perform in simple causal settings. After highlighting several deficiencies, we propose causal constraints for both measures. A comparison with explanatory power shows that the causal version of COU is one step ahead in simple causal settings. However, slightly increasing the complexity of the underlying causal structure shows that both measures can easily disagree with explanatory power. The upshot of this is that even sophisticated causally constrained measures for unification ultimately fail to track explanatory relevance. This shows that unification and explanation are not as closely related as many philosophers thought.

ABSTRACT. Responsibility allocation is a fundamental problem in the analysis of distributed systems: How do we attribute individual contributions to a joint outcome? Petri nets are a model of distributed (concurrent) systems in which actors are represented by transitions. We propose the notion of forward-responsibility of coalitions of such actors as the existence of a winning strategy in a game played against the remaining transitions, with the objective of avoiding bad places. In our formalisation we introduce a novel game model on Petri nets, where a central concept is precedence determining priorities between conflicting transitions. We show how to compute forward-responsibility in Petri nets via a reduction to imperfect information games and demonstrate the expressiveness of our framework by encoding existing models of responsibility allocation. This allows us to adopt a new perspective and attribute responsibility not only to actors, but also directly to actions.

ABSTRACT. Incorrect or incomplete specifications often give rise to critical AI safety risks, such as reward hacking and unpredictable edge-case behaviors. To prevent AI agents from exploiting these vulnerabilities, verification methods should perform checks under a variety of different and unexpected conditions, and this demands incorporating causal counterfactual reasoning. This is a preliminary work on sabotage logic which leverages different types of deletions and allows one to reason about the causal and counterfactual dependencies.

ABSTRACT. Propensity scores (PS) are an effective strategy for controlling for bias when estimating causal effects from observational data. Nevertheless, traditional methods often struggle with complex treatment structures beyond binary or discrete treatments. In this context, this work introduces a methodology for propensity score estimation that accommodates generalized treatment structures without imposing restrictive parametric assumptions. We use a probabilistic classification model to estimate stabilized weights and propensity scores via density-ratio estimation, making our method adaptable to various treatment forms. Experimental results show notable performance improvements in accuracy and stability across different synthetic and semi-synthetic datasets, even as the number of covariates increases. This suggests that our approach is flexible enough to be considered for challenging real-world applications in causal effect estimation, such as healthcare, policy analysis, and personalized marketing.

ABSTRACT. We address the problem of computing actual causality, as defined by Halpern and Pearl for the explanation of predictions made by Neural Networks. Most existing explanation methods assume feature independence, which can yield misleading explanations when inputs exhibit structured dependencies. We formalize explanations via Halpern and Pearl actual causality with SCMs, reducing cause search to a verification problem solved via differentiable relaxations and branch-and-bound. We perform preliminary experiments and show that our method outperforms state-of-the-art approaches in scalability and completeness.

ABSTRACT. Counterfactuals -- statements about what *might* have happened under different circumstances -- offer a natural way to phrase causal questions and have gained increasing prominence in machine learning, with applications ranging from medical decisions to discrimination. We argue that, while counterfactuals are powerful philosophical constructs, the computation of *individual* counterfactual trajectories is riddled with dangers. Individualized counterfactuals are often not useful or even harmful, because the required assumptions cannot be adequately justified or because counterfactuals are conceptually misaligned with what would be informative for the task at hand.

ABSTRACT. A prominent claim in the foundations of causal reasoning in artificial intelligence—most influentially associated with Judea Pearl—is that contemporary machine learning systems remain confined to associative reasoning and therefore lack genuine causal competence. According to this view, explicit structural causal models are a necessary prerequisite for answering interventional or counterfactual questions. We argue that current practice already challenges the strongest interpretation of this claim. Modern machine-learning-based systems, particularly when embedded in interactive or agentic settings, exhibit forms of behavior that cannot be cleanly classified as purely associative, including intervention-like reasoning, explanation-seeking dialogue, and responsibility attribution. The contribution is not to reject formal causal frameworks, but to expose a growing mismatch between formal definitions of causation and the descriptive reality of deployed computational systems. This mismatch raises foundational questions directly relevant to formal reasoning about causation, responsibility, and explanation.