Author name cluster

Daxin Liu

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

12 papers

1 author row

AAAI Conference 2026 Conference Paper

A Framework for Belief-based Programs and Their Verification (Abstract Reprint)

Daxin Liu
Gerhard Lakemeyer

Belief-based programming is a probabilistic extension of the GOLOG program family where every action and sensing result can 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 certain properties. At least two problems exist in verifying such programs: how to formally specify program properties and what is the complexity of the verification problem. In this paper, we propose a formalism for belief programs based on a modal logic of actions and beliefs which allows us to conveniently express PCTL-like temporal properties. We also investigate the decidability and undecidability of the verification problem.

PDF Details DOI

AAMAS Conference 2026 Conference Paper

Epistemic Modal Logic Meets Algebraic Model Counting

Daxin Liu
Vaishak Belle

Algebraicmodelcounting(AMC)generalizesweightedmodelcounting to the semiring setting and supports various types of labels (or weights), including numerical ones as used in weighted model counting, but also sets, boolean formulae, polynomials, and many more. One merit of algebraic model counting is that it can be evaluated efficiently in a succinct form of representation by using knowledge compilation, hence, providing a robust and useful framework that covers many different tasks from a variety of different fields. In this paper, we show that a type of epistemic entailment reasoning in a modal logic of only knowing can be solved by recursively calling a series of algebraic model counting tasks. We show that this approach is not limited to the qualitative setting, but is also applicable to the quantitative modal logic of only-believing. Lastly, we propose an AMC-based regression operator that lifts the approach to even dynamic epistemic reasoning.

PDF

JAIR Journal 2025 Journal Article

A Framework for Belief-based Programs and Their Verification

Daxin Liu
Gerhard Lakemeyer

PDF Details DOI

AAAI Conference 2025 Conference Paper

On Action Theories with Iterable First-Order Progression

Daxin Liu
Jens Claßen

We study the first-order definability of progression for situation calculus action theories with a focus on the iterability of progression. Progression, the task of updating a knowledge base according to actions' effects so that proper information is retained, is notoriously challenging as it in general requires second-order logic. Exceptions where progression is first-order like local-effect actions and normal actions impose certain syntax constraints on action theories to eliminate second-order quantifiers in the progressed knowledge base. Unfortunately, the progressed result might not satisfy the constraints again, making it impossible to apply first-order progression iteratively. In this paper, we first lift the existing result on first-order progression for normal actions by allowing disjunctions in the knowledge base. As a result, we obtain an action theory whose type is called disjunctive normal, which is iteratively first-order progressable. Second, we propose a new class of action theories, called PANACK, that strictly subsumes the disjunctive normal ones, and we show that it remains iteratively first-order progressable as well.

PDF Details DOI

AAMAS Conference 2025 Conference Paper

What Is a Counterfactual Cause in Action Theories?

Daxin Liu
Vaishak Belle

Since the proposal by Halpern and Pearl, reasoning about actual causality has gained increasing attention in artificial intelligence, ranging from domains such as model-checking and verification to reasoning about actions and knowledge. More recently, Batusov and Soutchanski proposed a notion of actual achievement cause in the situation calculus, amongst others, they can determine the cause of quantified effects in a given action history. While intuitively appealing, this notion of cause 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.

PDF

IJCAI Conference 2024 Conference Paper

First-Order Progression beyond Local-Effect and Normal Actions

Daxin Liu
Jens Claßen

One of the fundamental problems in reasoning about action is progression, which is to update a knowledge base according to the effects of an action into another knowledge base that retains all proper information. The problem is notoriously challenging, as in general, it requires second-order logic. Efforts have been made to find fragments where progression is first-order definable. Liu and Lakemeyer showed that for actions that have only local effects, progression is always first-order definable. They also generalized the result to so-called normal actions, that allow for non-local effects, as long as the affected fluent predicates only depend on local-effect ones, under certain restrictions on the knowledge base. In addition, they showed that for so-called proper+ knowledge bases, progression for normal actions can be efficient under reasonable assumptions. In this paper, we consider a larger class of theories, called the acyclic ones, that strictly subsumes normal actions. In such theories, dependencies between non-local effect fluent predicates are allowed, as long as they do not contain any cycles. We prove progression to be equally first-order definable for this class. Furthermore, under similar but stronger assumptions than those made by Liu and Lakemeyer, we show that progression is efficient as well.

PDF Details DOI

AAMAS Conference 2024 Conference Paper

Progression with Probabilities in the Situation Calculus: Representation and Succinctness

Daxin Liu
Vaishak Belle

Progression in the Situation Calculus is perhaps one of the most extensively studied cases of updating logical theories over a sequence of actions. While it generally requires second-order logic, several useful first-order and tractable cases have been identified. Recently, there has been an interest in studying the progression of probabilistic knowledge bases expressed using degrees of belief on first-order formulas. However, although a few results exist, they do not provide much clarity about how this progression can be computed or represented in a feasible manner. In this paper, we address this problem for the first time. We first examine the progression of a probabilistic knowledge base (PKB) in a world-level representation; in particular, we show that such a representation is closed under progression for any localeffect actions with quantifier-free contexts. We also propose a more succinct representation of the probabilistic knowledge base, i. e. factored-representation PKB. For this type of PKB, we study the conditions for progression to remain succinct.

PDF

AAMAS Conference 2023 Conference Paper

A Logic of Only-Believing over Arbitrary Probability Distributions

Qihui Feng
Daxin Liu
Vaishak Belle
Gerhard Lakemeyer

When it comes to robotic agents operating in an uncertain world, a major concern in knowledge representation is to better relate high-level logical accounts of beliefs and actions to the low-level probabilistic sensorimotor data. Perhaps the most general formalism for dealing with degrees of belief in formulas, and in particular, with how that should evolve in the presence of noisy sensing and acting is the first-order logical account by Bacchus, Halpern, and Levesque. The main advantage of such a logical account is that it allows a specification of beliefs that can be partial or incomplete, in keeping with whatever information is available about the domain, making it particularly attractive for general-purpose cognitive robotics. Recently, this model was extended to handle continuous probability distributions. However, it is limited to finitely many nullary fluents and defines beliefs and integration axiomatically, the latter making semantic proofs about beliefs and meta-beliefs difficult. In this paper, we revisit the continuous model and cast it in a modal language. We will go beyond nullary fluents and allow fluents of arbitrary arity as is usual in the standard situation calculus. This necessitates a new and general treatment of probabilities on possible worlds, where we define measures on uncountably many worlds that interpret infinitely many fluents. We then show how this leads to a fairly simple definition of knowing, degrees of belief, and onlyknowing. Properties thereof will also be analyzed. In this paper, we focus on the static setting and conclude with some thoughts about extending this account to actions as the next step and what challenges might arise.

PDF

KR Conference 2023 Conference Paper

Concerning Measures in a First-order Logic with Actions and Meta-beliefs

Daxin Liu
Qihui Feng
Vaishak Belle
Gerhard Lakemeyer

The unification of logic and probability has been seen as a long-standing concern in philosophy and mathematical logic. In this paper, we propose a new general probabilistic modal logic of belief and only-believing in the situation calculus. Our logic can express both continuous and discrete degrees of belief. More importantly, expressing degrees of belief for arbitrary first-order formulas in a dynamic setting is possible for the first time, going well beyond previous proposals where fluents are assumed to be nullary or discrete. We show that our notion of belief retains many of the properties known from the previous related work.

PDF Details DOI

AIJ Journal 2023 Journal Article

On the progression of belief

Daxin Liu
Qihui Feng

Based on weighted possible-world semantics, Belle and Lakemeyer recently proposed the logic DS, a probabilistic extension of a modal variant of the situation calculus with a model of belief. The logic has many desirable properties like full introspection and it is able to precisely capture the beliefs of a probabilistic knowledge base in terms of the notion of only-believing. While the proposal is intuitively appealing, it is unclear how to do planning with such logic. The reason behind this is that the logic lacks projection reasoning mechanisms and projection lies at the heart of planning. Projection reasoning, in general, is to decide what holds after actions. Two main solutions to projection exist: regression and progression. Roughly, regression reduces a query about the future to a query about the initial state while progression, on the other hand, changes the initial state according to the effects of actions and then checks whether the formula holds in the updated state. In this paper, we study projection by progression in the logic DS. It is known that the progression of a categorical knowledge base wrt a noise-free action corresponds to what is only-known after that action. We show how to progress a type of probabilistic knowledge base wrt noisy actions by the notion of only-believing after actions. Our notion of only-believing is closely related to Lin and Reiter's notion of progression.

Details DOI

KR Conference 2021 Conference Paper

On the Progression of Belief

Daxin Liu
Qihui Feng

Based on weighted possible-world semantics, Belle and Lakemeyer recently proposed the logic DS, a probabilistic extension of a modal variant of the situation calculus with a model of belief. The logic has many desirable properties like full introspection and it is able to precisely capture the beliefs of a probabilistic knowledge base in terms of the notion of only-believing. While the proposal is intuitively appealing, it is unclear how to do planning with such logic. The reason behind this is that the logic lacks projection reasoning mechanisms. Projection reasoning, in general, is to decide what holds after actions. Two main solutions to projection exist: regression and progression. Roughly, regression reduces a query about the future to a query about the initial state while progression, on the other hand, changes the initial state according to the effects of actions and then checks whether the formula holds in the updated state. In this paper, we study projection by progression in the logic DS. It is known that the progression of a categorical knowledge base wrt a noise-free action corresponds to what is only-known after that action. We show how to progress a type of probabilistic knowledge base wrt noisy actions by the notion of only-believing after actions. Our notion of only-believing is closely related to Lin and Reiter's notion of progression.

PDF Details DOI

IJCAI Conference 2021 Conference Paper

Reasoning about Beliefs and Meta-Beliefs by Regression in an Expressive Probabilistic Action Logic

Daxin Liu
Gerhard Lakemeyer

In a recent paper Belle and Lakemeyer proposed the logic DS, a probabilistic extension of a modal variant of the situation calculus with a model of belief based on weighted possible worlds. Among other things, they were able to precisely capture the beliefs of a probabilistic knowledge base in terms of the concept of only-believing. While intuitively appealing, the logic has a number of shortcomings. Perhaps the most severe is the limited expressiveness in that degrees of belief are restricted to constant rational numbers, which makes it impossible to express arbitrary belief distributions. In this paper we will address this and other shortcomings by extending the language and modifying the semantics of belief and only-believing. Among other things, we will show that belief retains many but not all of the properties of DS. Moreover, it turns out that only-believing arbitrary sentences, including those mentioning belief, is uniquely satisfiable in our logic. For an interesting class of knowledge bases we also show how reasoning about beliefs and meta-beliefs after performing noisy actions and sensing can be reduced to reasoning about the initial beliefs of an agent using a form of regression.

PDF Details DOI