A Non-Interventionist Approach to Causal Reasoning Based on Lewisian Counterfactuals

Authors: Carlos Aguilera-Ventura, Xinghan Liu, Emiliano Lorini, Dmitry Rozplokhas

IJCAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical We present a computationally grounded semantics for counterfactual conditionals... We show that this problem is PSPACE-complete and provide a reduction of it into QBF that can be used for automatic verification of causal properties. As far as we know, nobody before us provided a succinct formulation of the model checking problem for Lewis logic of counterfactual conditionals and a tight complexity result for this problem.
Researcher Affiliation Academia Carlos Aguilera-Ventura1, Xinghan Liu2, Emiliano Lorini1 and Dmitry Rozplokhas2 1IRIT, CNRS, Toulouse University, France 2TU Wien, Austria
Pseudocode No The paper only describes logical formulas and reductions (e.g., Sat(p, Xi) = vi p, Sat( ω, Xi) = bi ω, State(Xi) = ω Γ (bi ω Sat(ω, Xi)), Closest(φ, Xi, Xj) = Xk. r. State(Xk) (Sat(φ, Xk) r) ((Eq(Xj, Xk) r) (Closer(Xi, Xj, Xk) r))) rather than structured pseudocode or algorithm blocks. The computational aspects in Section 5 are more about logical transformations for model checking than step-by-step procedures.
Open Source Code No The paper mentions an extended version with proofs: 'The extended version of this paper with all proofs is available in https://arxiv.org/pdf/2505.12972.' This link is for the paper itself, not for any source code. There are no other statements about code release or links to source code repositories.
Open Datasets No The paper is theoretical, focusing on formalizing a new semantic approach and analyzing its complexity. It uses illustrative examples (e.g., 'Example 1 (Videogame)', 'Example 3. Suzy and Billy decide to throw a rock simultaneously') to explain concepts, but does not conduct experiments on, or provide access information for, any publicly available or open datasets.
Dataset Splits No This paper is theoretical and does not involve experimental evaluation on datasets. Therefore, it does not provide any specific information regarding training/test/validation dataset splits.
Hardware Specification No The paper is theoretical, focusing on formal frameworks and computational complexity. It does not describe any experiments that would require specific hardware, and thus, no hardware specifications are mentioned.
Software Dependencies No The paper discusses reducing the model checking problem to the Quantified Boolean Formula problem (QBF) for automatic verification but does not list any specific software dependencies or versions (e.g., programming languages, libraries, or solvers) used for implementation or experimentation.
Experiment Setup No As a theoretical paper, it does not present empirical experiments, and consequently, there is no description of an experimental setup, including hyperparameters or training configurations.