arXiv subjects

Daxin Liu

Publications and source records attributed to Daxin Liu.

3 recordsLinked to original sources

arXiv2026

On the Size Complexity and Decidability of First-Order Progression

Progression, the task of updating a knowledge base to reflect action effects, generally requires second-order logic. Identifying first-order special cases, by restricting either the knowledge base or action effects, has long been a central topic in reasoning about actions. It is known that local-effect, normal, and acyclic actions, three increasingly expressive classes, admit first-order progression. However, a systematic analysis of the size of such progressions, crucial for practical applications, has been missing. In this paper, using the framework of Situation Calculus, we show that under reasonable assumptions, first-order progression for these action classes grows only polynomially. Moreover, we show that when the KB belongs to decidable fragments such as two-variable first-order logic or universal theories with constants, the progression remains within the same fragment, ensuring decidability and practical applicability.

cs.AI↗

arXiv2025

A Counterfactual Cause in Situation Calculus

Perhaps the most popular modern formulation of actual causality is the HP account by Halpern and Pearl. Recent advancement has focused on extension of HP account to lift its limited expressiveness, in particular, Batusov and Soutchanski proposed a notion of actual achievement cause in the situation calculus, a rich first-order formalism of actions and changes. Among other things, the first-order nature allows for determining the cause of quantified effects in a given action history therein. While intuitively appealing, Batusov and Soutchanski's account is not defined in a counterfactual perspective. In this paper, we propose a notion of cause based on counterfactual analysis. In the context of action history, we show that our notion of cause generalizes naturally to a notion of achievement cause. We analyze the relationship between our notion of the achievement cause and the achievement cause by Batusov and Soutchanski. Finally, we relate our account of cause to Halpern and Pearl's account of actual causality. Particularly, we note some nuances in applying a counterfactual viewpoint to disjunctive effects, a common thorn in definitions of actual causes.

cs.AI↗

arXiv2022

On the Verification of Belief Programs

In a recent paper, Belle and Levesque proposed a framework for a type of program called belief programs, a probabilistic extension of GOLOG programs where every action and sensing result could be noisy and every test condition refers to the agent's subjective beliefs. Inherited from GOLOG programs, the action-centered feature makes belief programs fairly suitable for high-level robot control under uncertainty. An important step before deploying such a program is to verify whether it satisfies properties as desired. At least two problems exist in doing verification: how to formally specify properties of a program and what is the complexity of verification. In this paper, we propose a formalism for belief programs based on a modal logic of actions and beliefs. Among other things, this allows us to express PCTL-like temporal properties smoothly. Besides, we investigate the decidability and undecidability for the verification problem of belief programs.

cs.AI↗