Paper deep dive
Efficient Counterfactual Reasoning in ProbLog via Single World Intervention Programs
Saimun Habib, Vaishak Belle, Fengxiang He
Intelligence
Status: succeeded | Model: anthropic/claude-sonnet-4.6 | Prompt: intel-v1 | Confidence: 95%
Last extracted: 3/24/2026, 3:22:08 AM
Summary
This paper proposes Single World Intervention Programs (SWIPs), an efficient program transformation method for counterfactual reasoning in ProbLog (a Probabilistic Logic Programming language). Inspired by the Single-World Intervention Graph (SWIG) framework, SWIPs transform ProbLog programs by splitting clauses into observed and fixed components relevant to a counterfactual query, rather than duplicating the entire program as in Twin Networks. The approach reduces counterfactual reasoning to marginal inference over a simpler program, achieves ~35% reduction in inference time versus Twin Networks, relies on weaker independence assumptions, and is formally proven correct with respect to Structural Causal Model semantics.
Entities (23)
Relation Signals (20)
Single World Intervention Programs (SWIPs) → appliedto → ProbLog
confidence 99% · proposing an efficient program transformation for counterfactuals as Single World Intervention Programs (SWIPs) in ProbLog
Saimun Habib → authored → Efficient Counterfactual Reasoning in ProbLog via Single World Intervention Programs
confidence 99% · SAIMUN HABIB S.Habib-1@ed.ac.uk listed as author
Vaishak Belle → authored → Efficient Counterfactual Reasoning in ProbLog via Single World Intervention Programs
confidence 99% · VAISHAK BELLE vbelle@ed.ac.uk listed as author
Fengxiang He → authored → Efficient Counterfactual Reasoning in ProbLog via Single World Intervention Programs
confidence 99% · FENGXIANG HE F.He@ed.ac.uk listed as author
ProbLog → instanceof → Probabilistic Logic Programming (PLP)
confidence 99% · Probabilistic Logic Programming (PLP) languages, like ProbLog
SWIFT Algorithm → produces → Single World Intervention Programs (SWIPs)
confidence 99% · we introduce our Single-World Intervention Fact Transformation (SWIFT) algorithm detailed in Algorithm 3 to produce a Single World Intervention Program (SWIP)
Single World Intervention Programs (SWIPs) → proposedin → Efficient Counterfactual Reasoning in ProbLog via Single World Intervention Programs
confidence 99% · This paper addresses this challenge, by proposing an efficient program transformation for counterfactuals as Single World Intervention Programs (SWIPs) in ProbLog.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Probabilistic Logic Programming (PLP) languages, like ProbLog, naturally support reasoning under uncertainty, while maintaining a declarative and interpretable framework. Meanwhile, counterfactual reasoning (i.e., answering ``what if'' questions) is critical for ensuring AI systems are robust and trustworthy; however, integrating this capability into PLP can be computationally prohibitive and unstable in accuracy. This paper addresses this challenge, by proposing an efficient program transformation for counterfactuals as Single World Intervention Programs (SWIPs) in ProbLog. By systematically splitting ProbLog clauses to observed and fixed components relevant to a counterfactual, we create a transformed program that (1) does not asymptotically exceed the computational complexity of existing methods, and is strictly smaller in common cases, and (2) reduces counterfactual reasoning to marginal inference over a simpler program. We formally prove the correctness of our approach, which relies on a weaker set independence assumptions and is consistent with conditional independencies, showing the resulting marginal probabilities match the counterfactual distributions of the underlying Structural Causal Model in wide domains. Our method achieves a 35\% reduction in inference time versus existing methods in extensive experiments. This work makes complex counterfactual reasoning more computationally tractable and reliable, providing a crucial step towards developing more robust and explainable AI systems. The code is at this https URL.
Tags
Links
- Source: https://arxiv.org/abs/2603.20505v1
- Canonical: https://arxiv.org/abs/2603.20505v1
Trouble viewing inline? Open PDF directly →
Full Text
73,932 characters extracted from source content.
Expand or collapse full text
Efficient Counterfactual Reasoning in ProbLog via Single World Intervention Programs SAIMUN HABIB*† S.Habib-1@ed.ac.uk VAISHAK BELLE vbelle@ed.ac.uk FENGXIANG HE F.He@ed.ac.uk Abstract Probabilistic Logic Programming (PLP) languages, like ProbLog, naturally support reasoning under uncertainty, while maintaining a declarative and interpretable framework. Meanwhile, counterfactual reasoning (i.e., answering “what if” questions) is critical for ensuring AI systems are robust and trustworthy; however, integrating this capability into PLP can be computationally prohibitive and unstable in accuracy. This paper addresses this challenge, by proposing an efficient program transformation for counterfactuals as Single World Intervention Programs (SWIPs) in ProbLog. By systematically splitting ProbLog clauses to observed and fixed components relevant to a counterfactual, we create a transformed program that (1) does not asymptotically exceed the computational complexity of existing methods, and is strictly smaller in common cases, and (2) reduces counterfactual reasoning to marginal inference over a simpler program. We formally prove the correctness of our approach, which relies on a weaker set independence assumptions and is consistent with conditional independencies, showing the resulting marginal probabilities match the counterfactual distributions of the underlying Structural Causal Model in wide domains. Our method achieves a 35% reduction in inference time versus existing methods in extensive experiments. This work makes complex counterfactual reasoning more computationally tractable and reliable, providing a crucial step towards developing more robust and explainable AI systems. The code is at https://github.com/EVIEHub/swip. keywords: counterfactual reasoning, probabilistic logic programming, ProbLog, causality, single world intervention graph, structural causal models †journal: Theory and Practice of Logic Programming 1 Introduction Among causal queries, counterfactual questions of the form “What if X had been different?” are crucial for explanation, diagnosis, credit assignment, and decision making pearl_book_2018 ; halpern_actual_2019 . To situate its value, it is helpful to distinguish probabilistic, causal, and counterfactual modeling along Pearl’s “ladder of causality” pearl_causality_2009 . While probabilistic models describe associations, Structural Causal Models (SCMs) additionally specify directed functional relationships between variables with exogenous noise and how these relationships change under interventions pearl_causality_2009 . This hierarchy of associational, interventional, and counterfactual queries captures increasingly expressive forms of reasoning, and in particular, the capacity for counterfactual reasoning is a critical capability for artificial intelligence systems to discern effects of alternative choices by explicitly relating the actual world to hypothetical variants of a causal model’s structure under intervention to explain the observation(s) produced by the underlying generative mechanisms in either world gerstenberg_counterfactual_2024 ; epstude_functional . Why PLP?. Counterfactuals in SCMs traditionally followed a procedure of abduction, action, and prediction pearl_causality_2009 , but Hopkins and Pearl argue SCMs become unwieldy in realistic domains as they lack first-order expressivity over entity and attribute relationals, quantified rules, and temporally structured actions hopkins_causality_2007 . For example, the classic “two-riflemen” scenario pearl_causality_2009 requires a model that distinguishes multiple agents, possible misfires, and a disjunctive causal mechanism. A propositional encoding must enumerate each marksman A and B taking aim at a target and whether they hit the target separately, whereas a relational encoding expresses the causal mechanism compactly: hits(Target) :- fired(Soldier,Target). The broader lesson is that causal models benefit from symbolic structure, and symbolic systems benefit from principled causal semantics hopkins_causality_2007 . Probabilistic Logic Programming (PLP) sits naturally at this intersection. It provides explicit symbolic mechanisms as interpretable rules describing how entities and relations interact, combined with probabilistic uncertainty. Such rules (e.g., causes(Smoking,Cancer), infects(P1,P2)) support recursion, quantification, and relational generalization vennekens_cp-logic_2009 ; vennekens_embracing_2010 . However, strictly speaking PLP languages were not designed for causal inference pearl_causality_2009 ; vennekens_embracing_2010 ; vennekens_cp-logic_2009 ; DeRaedt.etal2007 . These languages lack a dodo-operator, formal intervention semantics, and tools for causal identification. A simple ProbLog program illustrates this gap: 0.3::lifestyle(alice). 0.3::smokes(alice). 0.6::genetic_risk(alice). cancer(alice) :- smokes(alice), genetic_risk(alice). Under distribution semantics, this program defines a joint probability over smokes(alice),genetic_risk(alice) smokes(alice), genetic\_risk(alice), and cancer(alice) with logical dependencies between them. Conditioning on smokes(alice)=false updates beliefs on Alice’s likelihood of cancer but does not implement the causal intervention (smokes(alice)=false)( smokes(alice)=false), which requires deleting the generative mechanism between smoking and cancer. This difference between conditioning and intervening marks the conceptual boundary between probabilistic and causal interpretation. Recognizing this limitation, several PLP languages extend logic programming with causal meaning. Logic Program Annotated Disjunctions (LPADs), vennekens_logic_2004 , Causal Probabilistic-logic (CP-logic) vennekens_cp-logic_2009 , and ProbLog DeRaedt.etal2007 introduce probabilistic choices, and CP-logic interprets rules as probabilistic causal laws. Its intervention semantics disable or modify such laws, aligning CP-logic with SCM-style reasoning. However, computing counterfactuals still follows the abduction, action, prediction procedure and requires storing the full posterior P(∣=)P(U =e) over exogenous causes U given the evidence or observations e . To address this, another line of work adapts the Twin Network construction from SCMs to ProbLog balke_probabilistic_2022 ; kiesel_what_2023 . Counterfactual inference is reduced to ordinary probabilistic inference by duplicating the program into factual and counterfactual copies linked by shared exogenous variables avoiding storing P(U∣E=e)P(U E=e) and doing intervention and inference at once to compute P(Y|do(X=x),E=e)P(Y|do(X=x),E=e). While convenient, this approach suffers from (i) exponentially many cross-world independence assumptions richardson_single_2013 ; Shpitser.etal2021 , and (i) demonstrable failures of these assumptions in important causal structures. In a practical sense, it is also limited for first-order relational models as it doubles program size, increasing compilation cost. 1.1 Our Contributions In this work, we introduce Single-World Intervention Programs (SWIPs), a new method for counterfactual reasoning in ProbLog inspired by the Single-World Intervention Graph (SWIG) framework richardson_single_2013 . Rather than duplicating the model, SWIPs perform a semantics-preserving transformation of the program itself. Returning to the earlier example, to compute P(cancer(alice)∣(smokes(alice)=0))P( cancer(alice) ( smokes(alice)=0)), SWIP removes the probabilistic fact 0.3::smokes(alice)., inserts the deterministic fact smokes(alice)=false., and manipulates the rule for cancer(alice). by removing its dependence on the original smoking mechanism while making it reliant on the intervention. More generally, given (X=x)(X=x), the SWIP transformation deletes all clauses defining X, inserts the deterministic fact(s) asserting :=X:=x in place of X, and eliminates redundant or unreachable rules through structural simplification. The resulting SWIP is a simplified ProbLog program whose distribution matches the counterfactual semantics of the corresponding SCM. SWIPs offer practical advantages. Across extensive synthetic experiments, SWIPs produce significantly smaller unfolded programs and reduce compilation and inference time by approximately 35% relative to Twin Networks. Since SWIPs simplify rather than duplicate rule structure, knowledge-compilation backends (d-DNNF, SHARPSAT) exploit the reduced treewidth directly eiter_treewidth-aware_2021 . We prove that (1) for any SCM encodable in ProbLog, SWIPs reproduce exactly the interventional and counterfactual distributions of the SCM under standard assumptions of unique supported models and faithful SCM encodings; (2) the SWIP approach is computationally less expensive than the Twin Network approach; and (3) the grounded SWIP semantics coincide with CP-logic’s intervention semantics, unifying event-based and equation-based causal interpretations. To our knowledge, SWIPs provide the first single-world, SCM-faithful counterfactual semantics inside ProbLog that avoid cross-world assumptions while retaining the expressive relational structure of logic programming. 2 Preliminaries 2.1 Causal Models and Counterfactuals A Structural Causal Model (SCM) ℳM is defined as a tuple ⟨,,ℱ⟩ ,V,F , where U are mutually independent exogenous variables, V are endogenous variables, and ℱ=fVV∈F=\f_V\_V is a set of structural equations of the form V:=fV(pa(V),UV),V:=f_V(pa(V),U_V), with pa(V)⊆pa(V) and UV⊆U_V . Each SCM induces a directed acyclic graph (DAG) G encoding the causal dependencies among variables pearl_causality_2009 . Figure 1 depicts a causal model between genetics G, lifestyle L, diet D, and health H while omitting the implicit exogenous noise variables for simplicity. LLDDHHGG Figure 1: A causal diagram with variables L, D, G, and H. The corresponding SCM declares H as a function of A, B and C, D as a function of G and L, and L as functions of G. An intervention replaces the equations for a subset ⊆X with constant assignments :=X:=x, producing a modified model ℳM_x. The induced post-interventional distribution is P(∣do(:=))=∏Vi∈∖XP(vi∣pa(Vi))⋅[x]in ℳ.P(v do(X:=x))= _V_i P(v_i (V_i))·I[x] M_x. Counterfactual queries, P(Y∣do(:=),=)P(Y do(X:=x),E=e), ask about outcomes under hypothetical interventions given observed evidence. Their computation typically follows the abduction, action, and prediction steps of balke_probabilistic_2022 . Abduction requires storing the entire distribution of Pℳ(U|E=e)P_M(U|E=e), while action manipulates the model ℳM into the intervened distribution ℳM_x for some assignment X:=xX:=x, and prediction finally calculates Pℳ(|=)P_M_ x(Y|E=e) pearl_causality_2009 ; balke_probabilistic_2022 ; kiesel_what_2023 , but the twin network circumvents the abduction step and combines action and prediction by taking ℳM and creating ℳKM^K given by the tuple ⟨U,V′∪V,ℱ⟩ ,V ,F . It sets V′=VV =V and uses it to create a factual and counterfactual set of equations with shared exogeneity defined as X:=fX(pa(X),UX),X∈VfX(pa(X)′,UX),X∈V′X:= casesf_X(pa(X),U_X), \,\,X \\ f_X(pa(X) ,U_X), X cases where pa(X)′=X′|X∈pa(X)pa(X) =\X |X∈ pa(X)\. Interventions are set on the variables in V′V , ie. X′:=xX :=x and we have: Pℳ(⋅|E=e,do(X:=x))=PℳxK(⋅|E=e)P_M(\,·\,|E=e,do(X:=x))=P_M_x^K(\,·\,|E=e) Alternatively, the Single-World Intervention Graph (SWIG) formalism provides a convenient graphical encoding of the abduction, action, and prediction steps used to evaluate counterfactuals richardson_single_2013 ; pearl_causality_2009 . Given a graph G encoding an SCM ℳM and an intervention do(X:=x)do(X:=x), a SWIG is obtained by splitting each intervened node X∈X into two: a factual copy X that receives incoming edges from pa(X)pa(X) and a fixed counterfactual copy X′:=xX :=x with outgoing edges to its original children. Exogenous variables remain as is, yielding a single graph that represents factual and counterfactual variables within one world while avoiding ad hoc duplication of independent noise sources. Following standard graphical separation criteria, the SWIG is a complete independence oracle and determines which counterfactual queries are identified by observed data richardson_single_2013 . 2.2 ProbLog ProbLog is a probabilistic logic programming language with distribution semantics DeRaedt.etal2007 . A ProbLog program P is a pair (LP(),Facts())(LP(P),Facts(P)). Facts()Facts(P) is a set of probabilistic facts of the form π::aπ::a, where a is a ground atom from the set of external propositions () E(B) and π∈[0,1]π∈[0,1] is its probability. These facts are assumed to be mutually independent and correspond to the exogenous variables U in an SCM. LP()LP(P) is a set of logical clauses (rules) of the form h←b1,…,bnh← b_1,…,b_n, where h is an internal proposition from ℑ() I(P) and the body b1,…,bn\b_1,…,b_n\ is a set of literals. These rules correspond to the structural equations ℱF in an SCM. The semantics of P define a probability distribution π _P over possible worlds ω, where a world is a complete truth assignment to all ground atoms in =()∪() B= J( B)∪ E( B). Formally, the probability of a world ω is π(ω)=∏ai∈ωπi∏ai∉ω(1−πi) _P(ω)= _a_i∈ω _i _a_i∉ω (1- _i ) for all probabilistic facts ai∈Facts(P)a_i∈ Facts(P), i.e., the product of the probabilities of all true probabilistic facts and the complements of those that are false. The probability of a query ϕφ is the sum of the probabilities of all worlds in which ϕφ is trueDeRaedt.etal2007 : π(ϕ)=∑ω⊧ϕπ(ω). _P(φ)= _ω φ _P(ω). For a ProbLog program to correctly represent an SCM, it must have unique supported models, meaning that for any truth assignment to the external propositions () E(P), the logical rules in LP()LP(P) must yield a single, unique truth assignment for all internal propositions ℑ() I(P). A sufficient condition for this property is that the dependency graph of LP()LP(P) is acyclic Kiesel.etal2023 . Within ProbLog, Pearl’s d-separation reasoning for independence and identifiability can be implemented declaratively as a meta-interpreter that encodes both the syntactic rules of do-calculus and the associated independence checks as higher-order logic predicates ruckschlos_subtlety_nodate . This enables automated symbolic reasoning about causal identifiability directly within the ProbLog environment. 3 Challenges of the Twin Network in ProbLog This section analyses a prevailing method for computing counterfactuals in ProbLog through a program transformation that constructs a Twin Network Kiesel.etal2023 . This approach operationalizes the SCM framework by creating a new ProbLog program, ()T(P), that explicitly represents both a factual and a counterfactual world. The transformation systematically duplicates all internal propositions ℑ() I(P) and their defining rules in LP()LP(P), while the external propositions in Facts()Facts(P) remain shared between the two worlds. This sharing of exogenous variables is the mechanism that relates the factual and counterfactual outcomes and the full procedure is detailed in Algorithm 1. This approach, however, implicitly relies on a strong and untestable cross-world assumption of all of these exogenous variables being independent of one another and in fact, the number of assumptions required grows at a doubly exponential rate Shpitser.etal2021 ; richardson_single_2013 . The duplication of the entire program by nature introduces higher compute cost for program compilation in proportion to the the program size and length of clauses in the program. In the worst case, it is Θ(||⋅Lmax) (|P|· L_ ) ϵL _LLϵG _GGϵD _DDϵH _HH (a) Original causal model ϵG _GϵL _LϵD _DϵH _HGGLLDDHHG∗G^*L∗L^*D∗D^*H∗H^* (b) Twin network with counterfactual variables Figure 2: Side-by-side comparison of (a) the original structural causal model and (b) its corresponding twin network construction. Theorem 3.1 (Twin Network Transformation Complexity) Let =(LP(),Facts())P=(LP(P),Facts(P)) be a ProbLog program with ||=|LP()|+|Facts()||P|=|LP(P)|+|Facts(P)| denoting the total number of clauses and facts. Let LmaxL_ be the maximum body length of any clause in LP()LP(P). Then the Twin Network transformation ()T(P) following Algorithm 2 from Kiesel et al. (2023) has complexity Θ(||⋅Lmax) (|P|· L_ ). An intervention do(X:=x)do(X:=x) is applied to the program by modifying the rules in the counterfactual part of the program. Subsequently, a counterfactual query Pℳ(Y|E=e)P_M^K_x(Y|E=e) is evaluated by computing a standard marginal probability on the transformed program ()T(P), as shown in Algorithm 2. The inference complexity itself is determined by an algorithm, such as knowledge compilation, whose runtime is given by a function g(w(G))g(w(G)) for a program with primal graph G of treewidth given by w(G)w(G) eiter_treewidth-aware_2021 . A necessary condition for the validity of this approach for a counterfactual queries is the original program P has unique supported models, for which a sufficient condition is an acyclic underlying logic program LP()LP(P). Algorithm 1 ConstructTwinNetwork(,do(X:=x))(P,do(X:=x)) 1:ProbLog program =(LP(),Facts())P=(LP(P),Facts(P)); intervention X:=xX:=x 2:Twin Network program ()T(P) 3:Initialize ()←∅T(P)← 4:for all p::a∈Facts()p::a (P) do 5: if a∈Xa then 6: Add 1.0::a1.0::a and 0.0::a′0.0::a to ()T(P) 7: else 8: Add p::ap::a and p::a′p::a to ()T(P) 9: end if 10:end for 11:for all h←b1,…,bn∈LP()h← b_1,…,b_n (P) do 12: if h∉Xh then 13: Add h←b1,…,bnh← b_1,…,b_n to ()T(P) 14: Add h′←b1′,…,bn′h ← b_1 ,…,b_n to ()T(P) 15: end if 16:end for 17:return ()T(P) Algorithm 2 EvaluateTwinNetworkQuery(,(),X:=x,E=e,ϕ)(P,T(P),X:=x,E=e,φ) 1:Original program P, Twin Network ()T(P), intervention X:=xX:=x, evidence E=eE=e, query formula ϕφ 2:Counterfactual probability π(ϕx|E=e) _P( _x|E=e) 3:p1←π(E=e)p_1← _P(E=e) 4:p2←π()(ϕ′∧E=e)p_2← _T(P)(φ =e) 5:return p2/p1p_2/p_1 4 Single World Intervention Programs To address both limitations, we introduce our Single-World Intervention Fact Transformation (SWIFT) algorithm detailed in Algorithm 3 to produce a Single World Intervention Program (SWIP) fit for a counterfactual query given an intervention and evidence. The SWIFT algorithm operationalizes the ”graph surgery” of Single-World Intervention Graphs richardson_single_2013 , shown in Figure 3, at the level of logical rules. Because rules interact through relational, quantified, and recursive dependencies, altering or deleting a clause may change the support, reachability, and logical structure of downstream atoms. The Twin Network approach avoids this by model duplication, at the cost of additional assumptions and computational overhead. Instead, the SWIFT algorithm provides a rule rewriting procedure that preserves the deterministic closure implied by existing rules and unique supported model requirement by the distribution semantics to produce a program semantically equivalent to the intervened Structural Causal Model. ϵL _LL L=lL=l ϵG _GGϵD _DDϵH _HH Figure 3: SWIG where intervention fix(L=l)fix(L=l) is acted To distinguish interventions in the Twin Network setting and the SWIP setting, we use the fix(X:=x)fix(X:=x) notation. This procedure first removes all clauses from LP()LP(P) that define the intervened propositions in X. This step corresponds to severing the causal arrows into the intervened nodes. Second, it iterates through the remaining rules and replaces any occurrence of an intervened atom Xi∈X_i in a rule body with a new, unique atom Xi,fixedX_i,fixed that represents its fixed value. This corresponds to redirecting the outgoing causal arrows from the original random node to the new fixed-value node. Finally, it adds deterministic facts to assert the values of these new fixed atoms. In contrast to constructing ()T(P), the complexity of SWIFT is at worst proportional to the program size, ie. when an intervened variable appears as an atom in every rule, while for ()T(P), it is always proportional. The resulting SWIP, ()S(P), is a valid ProbLog program that directly represents the counterfactual world. Theorem 4.1 (SWIP Transformation Complexity) Let =(LP(),Facts())P=(LP(P),Facts(P)) be a ProbLog program, and let ||=|LP()|+|Facts()||P|=|LP(P)|+|Facts(P)| denote the total number of clauses and facts. Let LmaxL_ be the maximum body length of any clause in LP()LP(P). Then the SWIP ()S(P) following Algorithm 3 has complexity O(||⋅Lmax)O(|P|· L_ ). As a corollary, it immediately follows Corollary 4.1.1 (Asymptotic Advantage of SWIFT over Twin Networks) Let =(LP(),Facts())P=(LP(P),Facts(P)) be a ProbLog program of size |||P|, and let LmaxL_ be the maximum body length of any clause in LP()LP(P). Let ()S(P) be the Single-World Intervention Program produced by the SWIFT transformation, and let ()T(P) be the Twin Network transformation of P. Then the time complexity of constructing ()S(P) is O(||⋅Lmax)O(|P|· L_ ), while the time complexity of constructing ()T(P) is Θ(||⋅Lmax) (|P|· L_ ). Moreover, ()S(P) is never asymptotically larger than ()T(P), and is strictly smaller whenever at least one intervened atom does not appear in all clause bodies. Algorithm 3 SWIFT(,fix(X:=x))(P,fix(X:=x)) 1:ProbLog program =(LP(),Facts())P=(LP(P),Facts(P)); intervention X:=xX:=x 2:Single-World Intervention Program ()S(P) 3:Initialize ()←Facts()S(P) (P) 4:Let LP−X←C∈LP():head(C)∉XLP_-X←C (P):head(C) 5:for all C=(h←b1,…,bn)∈LP−XC=(h← b_1,…,b_n)∈ LP_-X do 6: Let B′=b1′,…,bn′B =b_1 ,…,b_n be a new set of body literals 7: for all bj∈b1,…,bnb_j∈b_1,…,b_n do 8: Let a be the atom of the literal bjb_j. 9: if a∈Xa then 10: bj′←literal corresponding to afixed(xa)with the same sign as bjb_j corresponding to a_fixed(x_a)with the same sign as b_j. 11: else 12: bj′←bjb_j ← b_j 13: end if 14: end for 15: Add the rewritten rule h←B′h← B to ()S(P) 16:end for 17:for all Xi∈X_i do 18: Add the fact 1.0::Xi,fixed(xi)1.0::X_i,fixed(x_i) to ()S(P) 19:end for 20:return ()S(P) That is to say, while asymptotically equivalent in the worst case, SWIPs avoid unconditional duplication and are strictly smaller for sparse interventions. This directly translates to query speed ups in the general case, and in the worst case, is the same cost as querying over ()T(P). As shown in Algorithm 4, evidence is incorporated by adding facts to ()S(P), and the counterfactual probability is obtained via standard marginal inference on this final program. Algorithm 4 EvaluateSWIPQuery((),E=e,ϕ)(S(P),E=e,φ) 1:SWIP ()S(P); evidence E=eE=e; counterfactual query formula ϕφ 2:Counterfactual probability π()(ϕ|E=e) _S(P)(φ|E=e) 3:p1←π()(E=e)p_1← _S(P)(E=e) 4:p2←π()(ϕ∧E=e)p_2← _S(P)(φ =e) 5:return p2/p1p_2/p_1 Theorem 4.2 (Inference Complexity Comparison) Let g(⋅)g(·) be the complexity of some inference algorithm. Then inference complexity for querying over ()S(P) vs ()T(P) is O(g(w(())))≤O(g(w(())))O(g(w(S(P))))≤ O(g(w(T(P)))) Because our transformation is proven to yield a program whose semantics are equivalent to the counterfactual distribution of the underlying SCM, it inherits the established consistency with other causal formalisms like CP-logic and LPADs Kiesel.etal2023 ; vennekens_cp-logic_2009 ; vennekens_logic_2004 . Theorem 4.3 (Correctness of SWIP-Based Counterfactual Queries) Let P be a ProbLog program encoding a structural causal model M with unique supported models. Let ()=SWIFT(,fix(:=))S(P)=SWIFT(P,\,fix(X:=x)) be the SWIG-transformed program and let e()S^e(P) be the program augmented with evidence =E=e. Then for any query ϕφ under intervention x, πe()(ϕ)=πℳ(ϕx|E=e). _S^e(P)(φ)= _M( _x|E=e). These theorems suggest with respect to program construction, the Twin Network approach unconditionally duplicates the program, regardless of the intervention query while the SWIP approach scales slower with program size and maximum clause body length and at worst case, will incur the same cost as the Twin Network approach. In realistic applications, where programs and evidence sets may be large but interventions focused on a small subset of predicates, SWIPs can take advantage of the locality and specificity of the query structure. As a result, SWIPs naturally favor compact counterfactual representations and furthermore, are a more realistic approach for capturing real world counterfactuals. Beyond the issue of cross-world independence assumptions growing at a doubly exponential rate, richardson_single_2013 strongly emphasize the assumptions of the Twin Network are, by definition, mutually exclusive and thus, experimentally unverifiable. SWIGs, and by extension, SWIPs, ability to avoid this is especially salient in sequentially randomized trials and longitudinal decision problems. In such settings, treatments are assigned over time based on evolving histories, and counterfactual reasoning must respect the temporal and logical structure of these assignments. Richardson and Robins show that Twin Network constructions can induce incorrect independencies in these cases, whereas SWIGs preserve the correct causal structure by explicitly representing interventions as node-splitting operations within a single world richardson_single_2013 . Our results show that SWIPs inherit this advantage at the level of probabilistic logic programs: interventions modify only the clauses corresponding to treatment assignment mechanisms, while leaving downstream deterministic and probabilistic dependencies intact. We can characterize these counterfactual independence conclusions in PLP contexts when not using SWIPs and show our method is a more general and robust implementation of the SCM semantics and is consistent with CP-logic over the same set of models as the Twin Network. Theorem 4.4 (SWIP Consistency with LPAD ) Let P be a propositional LPAD-program such that every selection yields a logic program with a unique supported model. Let ,⊆X,E B be sets of propositions with value assignments x and e, respectively, and let ϕφ be a P-formula. Denote by πCP(ϕ∣E=e,fix(X:=x))π^CP_P(φ =e,fix(X:=x)) the counterfactual probability computed by CP-logic using the fixed-operator semantics on LPADs, and by πProb()SWIP(ϕ∣E=e,fix(X:=x))π^SWIP_Prob(P)(φ =e,fix(X:=x)) the counterfactual probability induced by the corresponding Single World Intervention Program (SWIP) constructed from Prob()Prob(P). Then, πCP(ϕ∣E=e,fix(X:=x))=πProb()SWIP(ϕ∣E=e,fix(X:=x)).π^CP_P(φ =e,fix(X:=x))\;=\;π^SWIP_Prob(P)(φ =e,fix(X:=x)). Theorem 4.5 (Consistency of SWIPs with CP-Logic) Let P be a ProbLog program with unique supported models, and let ,⊆X,E B with value assignments x and e. For any P-formula ϕφ, denote by πLPAD()CP(ϕ∣E=e,fix(X:=x))π^CP_LPAD(P)(φ =e,fix(X:=x)) the counterfactual probability defined via CP-logic on the LPAD-transformation of P, and by πSWIP(ϕ∣E=e,fix(X:=x))π^SWIP_P(φ =e,fix(X:=x)) the counterfactual probability computed by the SWIP semantics directly on P. Then, πLPAD()CP(ϕ∣E=e,fix(X:=x))=πSWIP(ϕ∣E=e,fix(X:=x)).π^CP_LPAD(P)(φ =e,fix(X:=x))\;=\;π^SWIP_P(φ =e,fix(X:=x)). For example, consider a simple power failure system that involves a deterministic relationship that creates a logical constraint. Let A be the main power supply, B the independent backup power supply, C an indicator for if the system is on, and D a deterministic report filed iff C is true. As a ProbLog program, P: % Exogenous variables for the two power supplies 0.5::u_a 0.5::u_b % Endogenous variables defined by structural rules a :- u_a. b :- u_b. c :- a. c :- b. d :- c. The atom a represents the main power being active, b represents the backup being active, c represents the system being on, and d represents the report being filed. The rule d :- c establishes the deterministic link. Now consider the query, ”Given we know the back up generator was on, is the report being filed independent of the main generator?” or formally, D⊥A|B=1D A|B=1. According to standard do-calculus on the Twin Network of this program, we see that D is not independent of A but of course, the status of A is no longer relevant as B=1B=1 fully informs us of D. Indeed, in the ProbLog d-separation metainterpreter by ruckschlos_subtlety_nodate , the twin network program will not reveal this dependency but it is trivially identified in the SWIP. The SWIG literature emphasizes that single-world node-splitting correctly exposes many counterfactual conditional independencies that cannot be read from a naive multi-world duplication via d-separation without further assumptions richardson_single_2013 . All d-separation claims in this paper are evaluated on the grounded dependency graph corresponding to the induced Structural Causal Model of the ProbLog program. Concretely, this graph is obtained by grounding the program and interpreting probabilistic facts as mutually independent exogenous variables and logical clauses as directed functional dependencies between endogenous variables. The following formal statement makes this concrete in the ProbLog setting and generalizes the power failure example. Theorem 4.6 (Misidentified Independencies in Twin Network Programs) Let P be a ProbLog program encoding an SCM ℳ=⟨,,ℱ⟩M= ,V,F . Suppose there exist distinct endogenous atoms A,B,D∈A,B,D such that: (1) D is defined in LP()LP(P) by a set of clauses whose combined effect is a deterministic function d=g(a,b,D)d=g(a,b,u_D) (possibly expressed via multiple rules), where Du_D denotes the exogenous input(s) relevant to D; (2) there exists a value b⋆b for B with the screening property g(a,b⋆,uD)=g(a′,b⋆,uD)∀a,a′ and all D,g(a,b ,u_D)=g(a ,b ,u_D) \ ∀ a,a and all u_D, i.e. when B=b⋆B=b the value of D is pointwise independent of A given the same exogenous input uDu_D; (3) A and B are not d-separated by the empty set in the causal graph underlying P and the program satisfies unique supported model conditions so the ProbLog semantics is well defined. Then the following hold: (a) On the SWIP for the intervention (B=b⋆)(B=b ) the node Db⋆D_b is d-separated from A (possibly conditioning on nothing or on appropriate observed variables), and hence the SWIP implies the counterfactual independence D⟂A|B=b∗D A|B=b^* (b) There exist programs P satisfying (1) - (3) for which the Twin Network construction ()T(P) does not d-separate the factual atom A from the counterfactual copy D∗D . Consequently, ordinary do-calculus on ()T(P) will not soundly identify the independence. In the power failure example, it is trivial to see this is a result of the direct dependency between D and C. However, the value of a counterfactual program transformation which is a complete independence oracle is highlighted by condition (1) of Theorem 4.6, where D may be expressed, unobviously, deterministically as a composition of multiple rules. The above results demonstrate the failure of the Twin Network is not a PLP issue nor can PLP alone reveal independencies in program structure when interventions are implemented across worlds ruckschlos_subtlety_nodate ; R_ckschlo__2023 . SWIPs, by design, align functional causal semantics with the interventional theory of CP-Logic while avoiding independence pathologies. 5 Experiments We’ve established that SWIPs can be used for counterfactual queries by reducing them to marginal inference and carry out this query via SharpSAT, a top down Knowledge Compilation korhonen_integrating_2021 . To assess the scalability and efficiency of our SWIP counterfactual inference method, we replicate and extend the experimental setup from kiesel_what_2023 . Our evaluation focuses on three primary questions: (i) how counterfactual program size varies with the SWIP approach and the Twin Network approach, (i) how inference time varies with program size and structural complexity, and (i) how inference time is affected by the number and type of evidence and intervention atoms. Benchmark Instances. Following kiesel_what_2023 , we generate acyclic directed graphs (DAGs) with a controlled size and treewidth. Each instance corresponds to a random probabilistic logic program modeling reachability in a directed graph. For a given graph G=(V,E)G=(V,E) with distinguished start and goal nodes s,g∈Vs,g∈ V, we encode the probability of reaching g from s using the following ProbLog schema: r(s). 0.1::trap(Y) :- p(X,Y). r(Y) :- p(X,Y). 1/d(X)::p(X, s 1(X));...;1/d(X)::p(X, s d(X)):- r(X), \+ trap(X). Here, d(X)d(X) denotes the out-degree of vertex X, and s_i(X) s\_i(X) denotes its i-th child node. The resulting program represents the random process of traversing the graph from s to g, avoiding nodes marked as traps. We vary two parameters controlling instance difficulty: the number of vertices n and the treewidth k. We first generate a random tree of size n using the networkx library (which has treewidth 11), and then add k additional nodes, each connected by incoming arcs from randomly selected original nodes. Finally, a single goal vertex g is added, receiving edges from each of the k new nodes. This procedure yields a DAG of size n+k+1n+k+1 with treewidth min(n,k) (n,k) and ensures acyclicity. For each instance, we sample up to five pieces of evidence and five interventions, allowing us to examine the interaction between query complexity and inference performance. Counterfactual queries are defined over this model by introducing positive or negative evidence on intermediate reachability predicates and positive or negative interventions on selected edges, following the schema: πℳ(r(g)|¬r(v1),…,¬r(vn),do(¬r(v1′)),…,do(¬r(vm′))),π^M_P (r(g)\,|\, r(v_1),…, r(v_n),do( r(v _1)),…,do( r(v _m)) ), for some evidence nodes v1,…,vnv_1,…,v_n and intervened nodes v1′,…,vm′v _1,…,v _m. ssv1v_1v…v_…v…v_…v…v_…v…v_…v…v_…vnv_nu1u_1u…u_…uku_kg Figure 4: Construction of benchmark DAGs. A random tree of size n rooted at s (top) is generated, a dense layer of k nodes u1,…,uku_1,…,u_k is added below (each receiving edges from multiple tree nodes), and a single goal node g is appended below the dense layer receiving edges from every uiu_i. All experiments were executed on the University of Edinburgh’s compute cluster. Each node is equipped with two Intel Xeon Gold 5218 CPUs (16 cores per CPU, 2.30 GHz base frequency), with 256 GB of DDR4 RAM per node operating at 2666 MHz. The cluster runs Red Hat Enterprise Linux 8.6 and uses the Slurm workload manager for parallel execution. We performed all experiments using Python 3.9.21 and ProbLog 2.2, with inference powered by the SHARPSAT knowledge compiler for top-down inference. This compiler was shown in kiesel_what_2023 to be fastest for counterfactual program query compilation. Each query was given a time limit of 1800 seconds; queries reaching the limit were assigned this maximum runtime for consistency with kiesel_what_2023 . 5.1 Results and Discussion Figure 5 shows the unfolded treewidths of the compiled ProbLog programs as a function of the synthetic graph size and original treewidth. As predicted, the SWIG-based transformation produces programs with substantially smaller unfolded treewidths than the Twin Network baseline. This difference arises because our approach performs a localized “graph surgery,” modifying only the clauses corresponding to intervened variables, rather than duplicating the entire logical program. By maintaining a single-world representation, the resulting dependency graph remains tighter and less entangled, leading to more compact knowledge-compilation structures. These smaller unfolded programs directly reduce the complexity of subsequent inference procedures, since treewidth is the dominant factor determining compilation cost in ProbLog-based inference Kiesel.etal2023 ; eiter_treewidth-aware_2021 ; korhonen_integrating_2021 . Figure 5: Unfolded treewidth as a function of synthetic graph size and original treewidth. The SWIG-based transformation yields narrower unfolded dependency structures than the Twin Network approach. This structural advantage translates directly into computational gains, as illustrated in Figure 6. Across all benchmark instances, the SWIG-based programs consistently compile and evaluate faster than their Twin Network counterparts. On average, our method requires approximately 65% of the runtime of the baseline for equivalent evidence and intervention configurations. The performance gap remains stable across varying program sizes and query complexities, confirming that reducing unfolded treewidth yields measurable improvements in both compilation and inference phases. Together, these results empirically validate that the SWIG-based transformation preserves the expressive and causal semantics of counterfactual reasoning while significantly improving computational efficiency. Figure 6: Mean compilation and inference times for varying numbers of evidence and intervention atoms. The SWIG-based transformation achieves lower inference and compilation times, corresponding to its smaller unfolded program structures. 6 Conclusion We have presented a SWIG-based approach to counterfactual reasoning in ProbLog. By “fixing” intervened nodes and propagating this intervention to descendant rules, we are able to reduce counterfactual queries to standard marginal inference queries. Our procedure of a transformation under intervention and subsequent evidence incorporation, is proven to yield the counterfactual distribution P(⋅∣do(X=x),E=e)P(· do(X=x),\,E=e) under assumptions of consistency and modularity. It also provides significant computational speedups in inference compared to existing approaches for counterfactual reasoning in ProbLog. In future work, it would be interesting to apply this approach to real-world settings and establishing counterfactual reasoning capabilities to DeepProbLog, an extension of ProbLog that combines it with neural network predicates to combine high level logical reason with low level subsymbolic perception manhaeve_neural_2021 . Furthermore, exploring σ-calculus, a more general form of do-calculus correa_calculus_2020 ; forre_constraint-based_2018 , to define counterfactuals for programs without unique supported models offers promising research directions. Acknowledgments Funding for this research was provided by NERC through an E4 DTP studentship (NE/S007407/1). References [1] J. Pearl and D. Mackenzie, The Book of Why: The New Science of Cause and Effect. USA: Basic Books, Inc., 1st ed., Apr. 2018. [2] J. Y. Halpern, Actual Causality. Cambridge, MA, USA: MIT Press, Feb. 2019. [3] J. Pearl, Causality. Cambridge: Cambridge University Press, 2 ed., 2009. [4] T. Gerstenberg, “Counterfactual simulation in causal cognition,” Trends in Cognitive Sciences, vol. 28, p. 924–936, Oct. 2024. [5] K. Epstude and N. J. Roese, “The Functional Theory of Counterfactual Thinking,” Personality and social psychology review : an official journal of the Society for Personality and Social Psychology, Inc, vol. 12, p. 168–192, May 2008. [6] M. Hopkins and J. Pearl, “Causality and Counterfactuals in the Situation Calculus,” Journal of Logic and Computation, vol. 17, p. 939–953, Oct. 2007. [7] J. Vennekens, M. Denecker, and M. Bruynooghe, “Cp-logic: A language of causal probabilistic events and its relation to logic programming,” Theory Pract. Log. Program., vol. 9, p. 245–308, May 2009. [8] J. Vennekens, M. Bruynooghe, and M. Denecker, “Embracing Events in Causal Modelling: Interventions and Counterfactuals in CP-Logic,” in Logics in Artificial Intelligence (T. Janhunen and I. Niemelä, eds.), (Berlin, Heidelberg), p. 313–325, Springer, 2010. [9] L. De Raedt, A. Kimmig, and H. Toivonen, “ProbLog: A probabilistic prolog and its application in link discovery,” in Proceedings of the 20th International Joint Conference on Artifical Intelligence, IJCAI’07, p. 2468–2473, Morgan Kaufmann Publishers Inc. [10] J. Vennekens, S. Verbaeten, and M. Bruynooghe, “Logic Programs with Annotated Disjunctions,” in Logic Programming (B. Demoen and V. Lifschitz, eds.), (Berlin, Heidelberg), p. 431–445, Springer, 2004. [11] A. Balke and J. Pearl, “Probabilistic Evaluation of Counterfactual Queries,” in Probabilistic and Causal Inference: The Works of Judea Pearl, vol. 36, p. 237–254, New York, NY, USA: Association for Computing Machinery, 1 ed., Mar. 2022. [12] R. Kiesel, K. Rückschloß, and F. Weitkämper, “”What if?” in Probabilistic Logic Programming,” May 2023. arXiv:2305.15318. [13] T. Richardson, “Single World Intervention Graphs ( SWIGs ) : A Unification of the Counterfactual and Graphical Approaches to Causality,” 2013. [14] I. Shpitser, T. S. Richardson, and J. M. Robins, “Multivariate Counterfactual Systems And Causal Graphical Models.” [15] T. Eiter, M. Hecher, and R. Kiesel, “Treewidth-Aware Cycle Breaking for Algebraic Answer Set Counting,” Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, vol. 18, p. 269–279, Sept. 2021. Conference Name: Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning. [16] R. Kiesel, K. Rückschloß, and F. Weitkämper, “”What if?” in Probabilistic Logic Programming.” [17] K. Rückschloß and F. Weitkämper, “On the Subtlety of Causal Reasoning in Probabilistic Logic Programming: A Bug Report about the Causal Interpretation of Annotated Disjunctions,” [18] K. Rückschloß and F. Weitkämper, “On the independencies hidden in the structure of a probabilistic logic program,” Electronic Proceedings in Theoretical Computer Science, vol. 385, p. 169–182, Sept. 2023. [19] T. Korhonen and M. Järvisalo, “Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper),” LIPIcs, Volume 210, CP 2021, vol. 210, p. 8:1–8:11, 2021. Artwork Size: 11 pages, 918439 bytes ISBN: 9783959772112 Medium: application/pdf Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [20] R. Manhaeve, S. Dumančić, A. Kimmig, T. Demeester, and L. De Raedt, “Neural probabilistic logic programming in DeepProbLog,” Artificial Intelligence, vol. 298, p. 103504, Sept. 2021. [21] J. Correa and E. Bareinboim, “A Calculus for Stochastic Interventions:Causal Effect Identification and Surrogate Experiments,” Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, p. 10093–10100, Apr. 2020. [22] P. Forré and J. M. Mooij, “Constraint-based Causal Discovery for Non-Linear Structural Causal Models with Cycles and Latent Confounders,” July 2018. arXiv:1807.03024 [stat]. Appendix A Notation and Definitions Table 1: Summary of key notation used throughout the paper. Symbol Definition V Set of endogenous variables U Set of exogenous variables ℱF Set of functional equations pa(X)pa(X) Set of endogenous parents of x ℳM Structural causal model (SCM): tuple of ⟨U,V,ℱ⟩ ,V,F X:=fX(pa(X),ϵX)X:=f_X(pa(X), _X) Structural equation for variable X w do(:=)do(X:=x) Pearl’s do-operator: modifies SCM equations of involving X fix(:=)fix(X:=x) Fix-operator: constructs a Single-World Intervention Graph ∗V^* Counterfactual copies of variables in the Twin Network ℳKM^K Twin Network SCM with shared exogenous variables P ProbLog program with logic and random facts LP()LP(P) Underlying logical clauses in a ProbLog program B Propositional alphabet for logic atoms ()T(P) Transformed Twin Network ProbLog program ()S(P) Transformed Single World Intervention Program Appendix B Proofs of Theorems 3.1, 4.1, 4.2 Proof B.1 (Proof of Theorem 3.1). Consider that for each fact r::A∈Facts()r::A (P), we either intervene on r if A is in the intervention set X or we add the observed and counterfactual facts to our program ()T(P). This has a complexity of Θ(|Facts()|) (|Facts(P)|). Similarly, for each clause C=h←b1,…,bn∈LP(P)C=h← b_1,…,b_n (P) with h∉Xh :, we add the clause and the counterfactual copy to ()T(P). Contructing the body of the counterfactual clause takes Θ(n) (n) per clause. Thus the total rule transformation complexity is: ∑C∈LP(P)Θ(|body(C)|)=Θ(|LP(P)|⋅Lmax) _C (P) (|body(C)|)= (|LP(P)|· L_ ) Summing these steps together we get a complexity of Θ(||⋅Lmax) (|P|· L_ ). Proof B.2 (Proof of Theorem 4.1). Analogous to Theorem 3.1, except we do not need to rewrite every clause, just the clauses with variables in the intervention set. Thus, we have O(||⋅Lmax)O(|P|· L_ ) Proof B.3 (Proof of Theorem 4.2). Let A be the set of internal atoms. Then ()T(P) contains approximately 2|A|2|A| atoms and rules. However, as the primal graph of ()T(P), denoted G()G_T(P), is constructed over the set of endogenous atoms A∪A∗A∪ A^* and no rule in ()T(P) contains both an atom from A and an atom from A∗A^* in its body, the resulting primal graph consists of two disconnected components. The treewidth of this composite graph, w(())w(T(P)), is therefore equal to the treewidth of the primal graph of the original program, w()w(P). Since inference (e.g., via knowledge compilation) has complexity as a function of treewidth, we have O(g(w(())))=O(g(w()))O(g(w(T(P))))=O(g(w(P))) Let G()G_S(P) be the primal graph of the transformed program ()S(P). Note that removing rules with heads in X deletes edges in GPG_P and that rewriting variables with fixed values does not add new dependencies. Therefore: w(())≤w(P)w(S(P))≤ w(P) Hence, inference complexity is: O(g(w(())))≤O(g(w(())))O(g(w(S(P))))≤ O(g(w(T(P)))) Appendix C Proofs of Theorem 4.4 and Theorem 4.5 To demonstrate the consistency of the SWIP treatment of counterfactuals with CP-logic we start by recalling the theory of CP-Logic from Vennekens et al. (2009) and the LPAD-programs of Vennekens et al. (2004) with their standard semantics. An LPAD program, P, is a finite set of rules of the following form: RC:=h1:π1;…;hl:πl←b1,…,bnRC:=h_1: _1;…;h_l: _l← b_1,…,b_n where hih_i and bib_i are atoms and literals in some set of propositions B. We have that the πi∈[0,1] _i∈[0,1] are associated probabilities for hih_i such that ∑iπi≤1 _i _i≤ 1. We define head(RC):=(h1,…,hl)head(RC):=(h_1,…,h_l) to be a tuple of propositions which are the head of RCRC, where h∈(h1,…,hl)h∈(h_1,…,h_l) if h=hih=h_i for a 1≤i≤l1≤ i≤ l and furthermore, l(RC):=l(RC):=l and hi(RC):=hih_i(RC):=h_i for 1≤i≤l1≤ i≤ l. Similarly, the body of RCRC is the finite set of literals body(RC):=b1,…,bnbody(RC):=\b_1,…,b_n\ A selection, σ, of P is a function σ:→ℕ∪⊥σ:P ∪\ \, where ⊥∉ℕ , that assigns to each LPAD-clause RC∈RC a natural number in [1,l][1,l] or σ(RC):=⊥σ(RC):= . To each selection σ, we associate a probability π(σ):=∏RC∈σ(RC)∈ℕπσ(RC)(RC)∏RC∈σ(RC)=⊥(1−∑i=1l(RC)πi(RC))π(σ):= _ subarraycRC \\ σ(RC) subarray _σ(RC)(RC) _ subarraycRC \\ σ(RC)= subarray (1- _i=1^l(RC) _i(RC) ) and each selection gives a logic program σ:=hσ(RC)←body(RC):RC∈,σ(RC)≠⊥.P^σ:=\h_σ(RC) (RC):RC ,σ(RC)≠ \. We define πdistπ^dist, the distribution semantics of P, as πdist(ϕ):=∑σ selectionσ⊧ϕπ(σ).π^dist_P(φ):= _ subarraycσ selection\\ P^σ φ subarrayπ(σ). where ϕφ is some P-formula. Rigguzi (2020) §2.4 establishes we can can translate an LPAD program P in B to a ProbLog program, Prob() Prob(P) where the logic of the program LP(Prob()LP(Prob(P) is given by choosing distinct propositions hiRC,ui(RC)∉h_i^RC,u_i(RC) ∈ B for all RC∈RC and natural number in [1,l][1,l] and letting hiRC←body(RC)∪¬hjRC∣1≤j<i∪ui(RC),h_i^RC (RC)∪\ h_j^RC 1≤ j<i\∪\u_i(RC)\, hi←hiRCh_i← h_i^RC Meanwhile, the random facts, Facts(Prob())Facts(Prob(P)) are defined as Facts(Prob()):=πi(RC)1−∏1≤j<iπj(RC)::ui(RC)|RC∈,1≤i≤l.Facts(Prob(P)):= \ _i(RC)1- _1≤ j<i _j(RC)::u_i(RC)\; |\;RC ,1≤ i≤ l \. This then ensures the following: Theorem C.1 (Riguzzi (2020), §2.4). Let P be a LPAD-program. Then, for every selection σ of P a set of possible worlds ℰ(σ)E(σ), which consists of all possible worlds ℰE such that ¬ui(RC) u_i(RC) holds unless σ(RC)≠⊥σ(RC)≠ or i>σ(RC)i>σ(RC) and such that uσ(RC)(RC)u_σ(RC)(RC) holds for every RC∈RC with σ(RC)≠⊥σ(RC)≠ . We conclude that σP^σ yields the same answer to every B-formula as the logic programs LP(Prob())∪ξLP(Prob(P))∪ξ for every ξ∈ℰ(σ)ξ (σ) and that π(ℰ(σ))=π(σ)π(E(σ))=π(σ). Further, the distribution semantics πdistπ^dist_P of P and the distribution semantics πProb()distπ^dist_Prob(P) of Prob()Prob(P) yield the same joint distribution on P. Conversely, we can turn each ProbLog program to an equivalent LPAD-Program. Again, Riguzzi (2020), §2.4 establishes for a ProbLog program P the LPAD-transformation LPAD()LPAD(P) is the LPAD-program that consists of one clause of the form u(RF):π(RF)←u(RF):π(RF)← for every random fact π(RF)::u(RF)π(RF)::u(RF) of P and a clause of the form head(LC):1←body(LC)head(LC):1 (LC) for every logic clause LC∈LP()LC (P). In this case, every selection σ of LPAD()LPAD(P) of probability not zero corresponds to a unique possible world ℰ(σ)E(σ), in which u(RC)u(RC) is true if and only if σ(RC)≠⊥σ(RC)≠ . Again, we obtain that the LPAD-transformation respects the distribution semantics. Theorem C.2 (Riguzzi (2020), §2.4). By the transformation of P to the LPAD program LPAD()LPAD(P), we have LP()∪ℰ(σ)LP(P) (σ) and LPAD()σLPAD(P)^σ yield the same answer to every P-formula. We also get that π(σ)=π(ℰ(σ))π(σ)=π(E(σ)). Hence, P and LPAD()LPAD(P) yield the same probability for every P-formula. Up until now, we have not differed from Kiesel et al. (2023) proof for showing the equivalence of interventions and counterfactuals in CP-Logic with SCMs by the dodo-operator in Twin Networks. However, to demonstrate that the equivalence holds under the fixfix-operator, we must extend the above theorems with the lemma which follows (and is proved) closely in style to Kiesel et al. (2023) Appendix B. Lemma C.3. Choose a proposition X∈X together with a truth value x. 1. In the situation of Theorem C.1, for every possible world ℰ∈ℰ(σ)E (σ) the logic programs fix(X:=x)σP^σ_fix(X:=x) and LP(Prob()fix(X:=x))∪ℰLP(Prob(P)_fix(X:=x)) yield the same answer to every P-formula. 2. In the situation of Theorem C.2, for every selection σ of LPAD()LPAD(P), the logic programs LPAD()fix(X:=x)σLPAD(P)^σ_fix(X:=x) and LP(Prob()fix(X:=x))∪ℰ(σ)LP(Prob(P)_fix(X:=x)) (σ) yield the same answer to every P-formula. Proof C.4. To prove (1), consider by Theorem B.1, for every P-formula ϕφ, σP^σ and LP(Prob())∪ℰLP(Prob(P)) will give the same answer to the query because in both programs are modular and consequently, their behavior is invariant to erasing clauses with X in the head or adding X←X←. More precisely, the SWIG style fix(X:=x)fix(X:=x)-operation in a LPAD/ProbLog syntactic setting is implemented by removing every head-option h:πh:π from every LPAD-clause whose head contains X, and adds some deterministic fact X←0/1X← 0/1. This implements the same surgical operations as used in implementing the dodo-operator in earlier proofs. If we fix a selection σ of P and let ℰ∈ℰ(σ)E (σ) be an arbitrary possible world corresponding to σ, then the translation Prob()Prob(P) introduces for each annotated disjunction in P a sequence of auxiliary atoms and random facts whose semantic effect is to pick exactly one head option (or none) according to the annotated probabilities. A selection σ corresponds to fixing which auxiliary random facts are true in a possible world ℰE of Prob()Prob(P); conversely ℰE determines σ. Performing the syntactic removals and additions that implement fix(X:=x)fix(X:=x) on σP^σ is equivalent to performing the corresponding removals and additions on the Prob()Prob(P) translation and then conjoining the choices represented by ℰE. Intuitively, the removals delete the same head-options in both syntaxes, and the deterministic additions become deterministic facts in the ProbLog encoding (or deterministic clauses whose head is an ordinary atom). Because logic programs are modular, if two programs differ only in clauses for a restricted set of atoms (here, the atoms in X and the auxiliary atoms that were introduced to encode choices for those rules), then the truth of a P-formula that mentions only other atoms remains unaffected. In particular, when we compare fix(X:=x)σP^σ_fix(X:=x) to LP(Prob()fix(X:=x))∪ℰLP(Prob(P)_fix(X:=x)) , all choices about auxiliary atoms (those in ℰE) are already fixed by ℰE, and the forced/blocked heads for atoms in X are syntactically identical in the two programs. It follows that the two programs produce the same derivations for all atoms and thus agree on the truth of every P-formula. For (2), we analogously apply Theorem B.2 but start with a selection σ of LPAD()LPAD(P). The construction of LPAD()σLPAD(P)^σ and the effect of fix(X:=x)fix(X:=x) on it correspond, under the ProbLog translation, to LP(Prob()fix(X:=x))LP(Prob(P)_fix(X:=x)) conjoined with the possible world ℰ(σ)E(σ) that encodes the selection σ. The same modularity and syntactic-translation observations as above show the two programs are extensionally identical (on atoms of interest) and therefore produce the same answers to every P-formula. □ From here, our proofs for Theorem 4 and 5 follows Kiesel et al. (2023) again. CP-logic estalishes a causal semantics for LPAD-programs. The semantics focus on P-processes and tying them to the logic of LPAD. More precisely, a P-process T is a tuple (T,ℐ)(T,I), where T is a directed tree and each edge is a labelled with a probability that describes transitioning from each node which are Humean events and. For each non-leaf node, the outgoing edges probabilities must sum to one. ℐI is a map that assigns each node n in T a Herbrand Interpretation ℐ(n)I(n) in B. Furthermore, for each n in T, we associate the probability πT(n)π^T(n) which is given by the product of the probabilities of all edges along the walk from root ⊥ of T to n. This produces a distribution πTπ^T on the Herbrand interpretations of I of B by π(I):=∑l leaf of T,ℐ(l)=Iπ(l).π^T(I):= _l leaf of T,\,I(l)=Iπ^T(l). Vennekens et al. (2009) connects LPAD-programs to P-processes by fixing a LPAD-program P and defining a hypothetical derivation sequence of n in T as a sequence of three valued interpretations (νi)0≤i≤n( _i)_0≤ i≤ n where ν0 _0 assigns False to all atoms not in ℐ(n)I(n) and for i>0i>0, there exists RC∈RC and j∈[1,l]j∈[1,l] with body(RC)νi≠Falsebody(RC) _i≠ False, with hji+1=Undefinedh_j^i+1=Undefined, and with νi(p)=νi+1(p) _i(p)= _i+1(p) for all other proposition p∈p . Such a sequence is terminal if it cannot be extended and each terminal hypothetical derivation sequence n has the same limit νn _n, which is known as the potential in n. For RC∈RC , we say that RCRC fires in a node n of T if for each 1<i<l(RC)1<i<l(RC) there exists a child nin_i of n such that ℐ(ni)=ℐ(n)∪hi(RC)I(n_i)=I(n)∪\h_i(RC)\ and such that each edge (n,ni)(n,n_i) is labeled with πi(RC) _i(RC). Moreover, there exists a child nl(RC)+1n_l(RC)+1 of n with ℐ(nl(RC)+1)=ℐ(n)I(n_l(RC)+1)=I(n). Let ℛℰ(n)R_E(n) denotes the set of all rules RC∈RC , for which there exists no ancestor a of n with ℰ(a)=RCE(a)=RC. Then, T then may be an execution model of P, ⊧T , if there exists a mapping ℰE from the non-leaf nodes of T to P such that: 1. ℐ(⊥)=∅I( )= for the root ⊥ of T. 2. In each non-leaf node n a LPAD-clause ℰ(n)∈ℛℰ(n)E(n) _E(n) fires with ℐ(n)⊧body(ℰ(n))I(n) (E(n)). 3. For each leaf l of T there exists no LPAD-clauses RC∈ℛℰ(l)RC _E(l) with ℐ(l)⊧body(RC)I(l) (RC). 4. For every node n of T we find body(ℰ(n))νn≠Undefined(E(n)) _n≠ Undefined, where νn _n is the potential in n. If ⊧T , then the probability distribution defined by πCP:=π^CP_P:=π^T matches the distribution semantics πdistπ^dist_P and implies the following. Lemma C.5 (Vennekens et al. (2009), §A.2). Let l be a leaf node in an execution model T of the LPAD-program P. In this case, there exists a unique path p from the root ⊥ of T to l. Define the selection σ(l)σ(l) by setting σ(l)(RC):=i∈ℕσ(l)(RC):=i if and only if there exists a node njn_j along p with ℰ(nj)=RCE(n_j)=RC and ℐ(nj+1):=ℐ(nj)∪hi(RC)I(n_j+1):=I(n_j)∪\h_i(RC)\. Otherwise, we set σ(l)(RC):=⊥σ(l)(RC):= . In this way, we obtain that σ(l)⊧ℐ(l)P^σ(l) (l). On the other hand, we find for each selection σ of P a leaf l of T with σ(l)=σ(l)=σ. To finally demonstrate the equivalence of this treatment of counterfactuals to CP-logic, consider the presentation of interventions and counterfactuals in CP-logic from Vennekens et al. (2010). Algorithm 5 Treatment of Counterfactuals in CP-logic 1::=,=⊆X:=x,E=e , P-formula ϕφ. 2:Counterfactual probability πCP(ϕ∣E=e,do(X:=x))π^CP_P(φ E=e,do(X:=x)). 3:Choose an execution model T of P. 4:for each leaf l of T do 5: Intervene in the logic program σ(l)P^σ(l) according to X:=xX:=x to obtain σ(l),do(X:=x)P^σ(l),do(X:=x). 6: Define πl(ϕ):=1,ℐ(l)⊧(E=e)∧σ(l),do(X:=x)⊧ϕ0,else.π^l(φ):= cases1,&I(l) (E=e)\; \;P^σ(l),do(X:=x) φ\\ 0,&else. cases 7:end for 8:Return πCP(ϕ∣E=e,do(X:=x)):=∑l leaf of πl(ϕ)⋅πCP(ℐ(l)∣E=e).π^CP_P(φ E=e,do(X:=x)):= _l leaf of Tπ^l(φ)·π^CP_P(I(l) E=e). As we have established in Lemma C.3, we can analogously posit that with the rewiring of clauses under the fixfix-operator the following algorithm: Algorithm 6 Fixed Operator Counterfactuals in CP-logic 1::=,=⊆X:=x,E=e , P-formula ϕφ. 2:Counterfactual probability πCP(ϕ∣E=e,fix(X:=x))π^CP_P(φ E=e,fix(X:=x)). 3:Choose an execution model T of P. 4:for each leaf l of T do 5: Intervene in the logic program σ(l)P^σ(l) according to X:=xX:=x to obtain σ(l),fix(X:=x)P^σ(l),fix(X:=x). 6: Define πl(ϕ):=1,ℐ(l)⊧(E=e)∧σ(l),fix(X:=x)⊧ϕ0,else.π^l(φ):= cases1,&I(l) (E=e)\; \;P^σ(l),fix(X:=x) φ\\ 0,&else. cases 7:end for 8:Return πCP(ϕ∣E=e,fix(X:=x)):=∑l leaf of πl(ϕ)⋅πCP(ℐ(l)∣E=e).π^CP_P(φ E=e,fix(X:=x)):= _l leaf of Tπ^l(φ)·π^CP_P(I(l) E=e). With these preparations we can now turn to the proof of the desired consistency results: Proof C.6 (Proof of Theorem 4.4). By Theorem 6, Lemma 9 and Lemma 8 the right-hand side of (B2) for P is the sum of the conditional probabilities π(ℰ|E=e)π(E|E=e) of all possible worlds ℰE of Prob()(P) such that ℳ(ℰ,LP(Prob()do(X:=x)))⊧ϕandℳ(ℰ,LP(Prob()))⊧(E=e).M (E,LP(Prob(P)^do(X:=x)) ) φ (E,LP(Prob(P))) (E=e). These are exactly the possible worlds that make the query ϕφ true after intervention while the observation E=eE=e is true before intervening. Hence, we can consult the proof of Theorem 3 to see that (B1) computes the same value as Algorithm 6. Proof C.7 (Proof of Theorem 4.5). By Theorem 7, Lemma 8 and Lemma 9 the right-hand side of (B2) for LPAD()(P) is the sum of the conditional probabilities π(ℰ|E=e)π(E|E=e) of all possible worlds ℰE of P such that ℳ(ℰ,LP(do(X:=x)))⊧ϕandℳ(ℰ,LP())⊧(E=e).M (E,LP(P^do(X:=x)) ) φ (E,LP(P)) (E=e). These are exactly the possible worlds that make the query ϕφ true after intervention while the observation E=eE=e is true before intervening. Hence, we can consult the proof of Theorem 3 to see that (B1) computes the same value as Algorithm 6. Appendix D Proof of Theorem 5.1 Proof D.1. We summarize notation from Kiesel et al. (2023) Kiesel.etal2023 . First, we define two propositional alphabets S P^S to handle the evidence from the source world and I P^I to handle the interventions in the counterfactual. In particular, we set e(S)=e()andi(I)=i(),e( P^S)\;=\;e( P) i( P^I)\;=\;i( P), and we require that S∩I=∅ P^S\;∩\; P^I\;=\; In this way, we obtain maps e/i:→S/Ibyp↦pS/I,e/i:\; P\;→\; P^\,S/I p\; \;p^\,S/I, that easily generalize to literals, clauses, and programs. Furthermore, we define the counterfactual semantics of P by K=S∪I.P^K\;=\;P^S\;∪\;P^I. Next, we intervene in KP^K for the counterfactual query is for the probability of a consequent ϕIφ^I in the interventional world given evidence ES=eE^S=e in the source world, after applying an intervention fix(X:=x)fix(X:=x) to the interventional part of the program. Let PK,fix(X:=x)P^K,fix(X:=x) denote this modified program given by Algorithm 3. Finally, we obtain the desired probability πPSCM(ϕ∣E=e,fix(X:=x))π^SCM_P(\,φ =e,\;fix(X:=x)\,) by querying the program PK,fix(X:=x)P^K,fix(X:=x) for the conditional probability π(ϕ∣E=e)π(φ =e). πSCM(ϕ∣=,fix(=)) _P^SCM(φ =e,\,fix(X=x)) :=πK,fix(:=)(ϕI∣S=) := _P^K,fix(X:=x)(φ^I ^S=e) =πK,fix(:=)(ϕI∧S=)πK,fix(:=)(S=) = _P^K,fix(X:=x)(φ^I ^S=e) _P^K,fix(X:=x)(E^S=e) =πK,fix(:=)(ϕI∧S=)πK(S=) = _P^K,fix(X:=x)(φ^I ^S=e) _P^K(E^S=e) =1πK(S=)∑επK(ε)⋅[ε⊧fix(:=)K(ϕI∧S=)] = 1 _P^K(E^S=e) _ _P^K( )·[ _P^K_fix(X:=x)(φ^I ^S=e)] =1π(=)∑επ(ε)⋅[ε⊧KS=]⋅[ε⊧fix(:=)KϕI] = 1 _P(E=e) _ _P( )·[ _P^KE^S=e]·[ _P^K_fix(X:=x)φ^I] =∑επ(ε)⋅[ε⊧=]⋅[ε⊧ℳxϕ]∑επ(ε)⋅[ε⊧=] = _ _P( )·[ =e]·[ _M_xφ] _ _P( )·[ =e] =PSCM(ϕ←,=)PSCM(=) = P_SCM( _X ,E=e)P_SCM(E=e) =PSCM(ϕ∣=,fix(:=)) =P_SCM(φ =e,\,fix(X:=x))