Fangzhen Lin

IJCAI Conference 2025 Conference Paper

Deduction with Induction: Combining Knowledge Discovery and Reasoning for Interpretable Deep Reinforcement Learning

• Haodi Zhang
• Xiangyu Zeng
• Junyang Chen
• Yuanfeng Song
• Rui Mao
• Fangzhen Lin

Deep reinforcement learning (DRL) has achieved remarkable success in dynamic decision-making tasks. However, its inherent opacity and cold start problem hinder transparency and training efficiency. To address these challenges, we propose HRL-ID, a neural-symbolic framework that combines automated rule discovery with logical reasoning within a hierarchical DRL structure. HRL-ID dynamically extracts first-order logic rules from environmental interactions, iteratively refines them through success-based updates, and leverages these rules to guide action execution during training. Extensive experiments on Atari benchmarks demonstrate that HRL-ID outperforms state-of-the-art methods in training efficiency and interpretability, achieving higher reward rates and successful knowledge transfer between domains.

AAMAS Conference 2025 Conference Paper

Hierarchical Learning-based Graph Partition for Large-scale Vehicle Routing Problems

• Yuxin Pan
• Ruohong Liu
• Yize Chen
• Zhiguang Cao
• Fangzhen Lin

Neural solvers based on the divide-and-conquer approach for Vehicle Routing Problems (VRPs) in general, and capacitated VRP (CVRP) in particular, integrates the global partition of an instance with local constructions for each subproblem to enhance generalization. However, during the global partition phase, misclusterings within subgraphs have a tendency to progressively compound throughout the multi-step decoding process of the learning-based partition policy. This suboptimal behavior in the global partition phase, in turn, may lead to a dramatic deterioration in the performance of the overall decomposition-based system, despite using optimal local constructions. To address these challenges, we propose a versatile Hierarchical Learning-based Graph Partition (HLGP) framework, which is tailored to benefit the partition of CVRP instances by synergistically integrating global and local partition policies. Specifically, the global partition policy is tasked with creating the coarse multi-way partition to generate the sequence of simpler two-way partition subtasks. These subtasks mark the initiation of the subsequent K local partition levels. At each local partition level, subtasks exclusive for this level are assigned to the local partition policy which benefits from the insensitive local topological features to incrementally alleviate the compounded errors. This framework is versatile in the sense that it optimizes the involved partition policies towards a unified objective harmoniously compatible with both reinforcement learning (RL) and supervised learning (SL). Additionally, we decompose the synchronized training into individual training of each component to circumvent the instability issue. Furthermore, we point out the importance of viewing the subproblems encountered during the partition process as individual training instances. Extensive experiments conducted on various CVRP benchmarks demonstrate the effectiveness and generalization of the HLGP framework. The source code is available at https: //github. com/panyxy/hlgp_cvrp. This work is licensed under a Creative Commons Attribution International 4. 0 License. Proc. of the 24th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2025), Y. Vorobeychik, S. Das, A. Nowé (eds.), May 19 – 23, 2025, Detroit, Michigan, USA. © 2025 International Foundation for Autonomous Agents and Multiagent Systems (www. ifaamas. org).

NeurIPS Conference 2025 Conference Paper

Multi-Task Vehicle Routing Solver via Mixture of Specialized Experts under State-Decomposable MDP

• Yuxin Pan
• Zhiguang Cao
• Chengyang GU
• Liu Liu
• Peilin Zhao
• Yize Chen
• Fangzhen Lin

Existing neural methods for multi-task vehicle routing problems (VRPs) typically learn unified solvers to handle multiple constraints simultaneously. However, they often underutilize the compositional structure of VRP variants, each derivable from a common set of basis VRP variants. This critical oversight causes unified solvers to miss out the potential benefits of basis solvers, each specialized for a basis VRP variant. To overcome this limitation, we propose a framework that enables unified solvers to perceive the shared-component nature across VRP variants by proactively reusing basis solvers, while mitigating the exponential growth of trained neural solvers. Specifically, we introduce a State-Decomposable MDP (SDMDP) that reformulates VRPs by expressing the state space as the Cartesian product of basis state spaces associated with basis VRP variants. More crucially, this formulation inherently yields the optimal basis policy for each basis VRP variant. Furthermore, a Latent Space-based SDMDP extension is developed by incorporating both the optimal basis policies and a learnable mixture function to enable the policy reuse in the latent space. Under mild assumptions, this extension provably recovers the optimal unified policy of SDMDP through the mixture function that computes the state embedding as a mapping from the basis state embeddings generated by optimal basis policies. For practical implementation, we introduce the Mixture-of-Specialized-Experts Solver (MoSES), which realizes basis policies through specialized Low-Rank Adaptation (LoRA) experts, and implements the mixture function via an adaptive gating mechanism. Extensive experiments conducted across VRP variants showcase the superiority of MoSES over prior methods.

NeurIPS Conference 2025 Conference Paper

Pixel Reasoner: Incentivizing Pixel Space Reasoning via Curiosity-Driven Reinforcement Learning

• Alex Su
• Haozhe Wang
• Weiming Ren
• Fangzhen Lin
• Wenhu Chen

Chain-of-thought reasoning has significantly improved the performance of Large Language Models (LLMs) across various domains. However, this reasoning process has been confined exclusively to textual space, limiting its effectiveness in visually intensive tasks. To address this limitation, we introduce the concept of pixel-space reasoning. Within this novel framework, Vision-Language Models (VLMs) are equipped with a suite of visual reasoning operations, such as zoom-in and select-frame. These operations enable VLMs to directly inspect, interrogate, and infer from visual evidences, thereby enhancing reasoning fidelity for visual tasks. Cultivating such pixel-space reasoning capabilities in VLMs presents notable challenges, including the model’s initially imbalanced competence and its reluctance to adopt the newly introduced pixel-space operations. We address these challenges through a two-phase training approach. The first phase employs instruction tuning on synthesized reasoning traces to familiarize the model with the novel visual operations. Following this, a reinforcement learning (RL) phase leverages a curiosity-driven reward scheme to balance exploration between pixel-space reasoning and textual reasoning. With these visual operations, VLMs can interact with complex visual inputs, such as information-rich images or videos to proactively gather necessary information. We demonstrate that this approach significantly improves VLM performance across diverse visual reasoning benchmarks. Our 7B model, Pixel-Reasoner, achieves 84% on V* bench, 74% on TallyQA-Complex, and 84% on InfographicsVQA, marking the highest accuracy achieved by any open-source model to date. These results highlight the importance of pixel-space reasoning and the effectiveness of our framework.

KR Conference 2025 Conference Paper

Pruning with Belief Traps in Multi-agent Epistemic Planning

• Biqing Fang
• Fangzhen Lin

Multi-agent epistemic planning (MEP) addresses planning problems involving multiple agents with epistemic reasoning, often requiring the consideration of nested beliefs. In this paper, we extend the notion of traps in classical planning to MEP, and call them belief traps, which are epistemic formulas that once entailed by an epistemic state, remain entailed by all successor states. Identifying belief traps can sometimes improve MEP solving significantly. Here, we consider two methods for identifying and using belief traps to improve planning efficiency. Our first method adapts a classical preprocessing algorithm with integration into an MEP planner, simple-form construction of traps, and a novel use of beneficial traps to guide search. The second method systematically generalizes the belief lock strategy by formalizing its underlying preservation condition. Our experiments show that the new pruning techniques can accelerate problem-solving in the domains with irreversible beliefs.

AAMAS Conference 2025 Conference Paper

Single-Agent Planning in a Multi-Agent System: A Unified Framework for Type-Based Planners

• Fengming Zhu
• Fangzhen Lin

We consider a general problem where an agent is in a multi-agent environment and must plan for herself without any prior information about her opponents. At each moment, this pivotal agent is faced with a trade-off between exploiting her currently accumulated information about the other agents and exploring further to improve future (re-)planning. We propose a theoretic framework that unifies a spectrum of planners for the pivotal agent to address this trade-off. The planner at one end of this spectrum aims to find exact solutions, while those towards the other end yield approximate solutions as the problem scales up. Beyond theoretical analysis, we also implement 13 planners and conduct experiments in a specific domain called multi-agent route planning with the number of agents up to 50, to compare their performaces in various scenarios. One interesting observation comes from a class of planners that we call safe-agents and their enhanced variants by incorporating domain-specific knowledge, which is a simple special case under the proposed general framework, but performs sufficiently well in most cases. Our unified framework, as well as those induced planners, provides new insights on multi-agent decision-making, with potential applications to related areas such as mechanism design.

NeurIPS Conference 2025 Conference Paper

VL-Rethinker: Incentivizing Self-Reflection of Vision-Language Models with Reinforcement Learning

• Haozhe Wang
• Chao Qu
• Zuming Huang
• Wei Chu
• Fangzhen Lin
• Wenhu Chen

Recently, slow-thinking systems like GPT-o1 and DeepSeek-R1 have demonstrated great potential in solving challenging problems through explicit reflection. They significantly outperform the best fast-thinking models, such as GPT-4o, on various math and science benchmarks. However, their multimodal reasoning capabilities remain on par with fast-thinking models. For instance, GPT-o1's performance on benchmarks like MathVista, MathVerse, and MathVision is similar to fast-thinking models. In this paper, we aim to enhance the slow-thinking capabilities of vision-language models using reinforcement learning (without relying on distillation) to advance the state of the art. First, we adapt the GRPO algorithm with a novel technique called Selective Sample Replay (SSR) to address the vanishing advantages problem. While this approach yields strong performance, the resulting RL-trained models exhibit limited self-reflection or self-verification. To further encourage slow-thinking, we introduce Forced Rethinking, which appends a rethinking trigger token to the end of rollouts in RL training, explicitly enforcing a self-reflection reasoning step. By combining these two techniques, our model, VL-Rethinker, advances state-of-the-art scores on MathVista, MathVerse to achieve 80. 4%, 63. 5% respectively. VL-Rethinker also achieves open-source SoTA on multi-disciplinary benchmarks such as MathVision, MMMU-Pro, EMMA, and MEGA-Bench, narrowing the gap with OpenAI-o1. We conduct comprehensive ablations and analysis to provide insights into the effectiveness of our approach.

KR Conference 2024 Conference Paper

Heuristic Strategies for Accelerating Multi-Agent Epistemic Planning

• Biqing Fang
• Fangzhen Lin

Multi-agent epistemic planning (MEP) is about achieving an epistemic goal in a multi-agent environment using agents’ actions that have epistemic preconditions and effects. Recently, MEP has received interest from both the dynamic logic and planning communities, leading to the development of several innovative planners. One such state of the art planner is MEPK. In this paper, we propose two novel strategies to enhance the search methods within MEPK. Our first strategy, the enhancement strategy, dynamically updates the heuristic based on the search path to the first goal-reachable node, potentially reducing the number of nodes that need to be explored to find a solution. Our second, the belief lock strategy, prevents the planner from continuing to search a particular state that cannot progress to a goal state due to the possession by an agent of a certain belief. Our experiments on existing benchmarks show that the new strategies can indeed accelerate the problem solving. We also construct new harder instances and demonstrate that our strategies significantly improve the performance on these hard benchmarks. Overall, we consider our new planner a significant improvement over the existing one in terms of computational efficiency.

NeurIPS Conference 2023 Conference Paper

Adjustable Robust Reinforcement Learning for Online 3D Bin Packing

• Yuxin Pan
• Yize Chen
• Fangzhen Lin

Designing effective policies for the online 3D bin packing problem (3D-BPP) has been a long-standing challenge, primarily due to the unpredictable nature of incoming box sequences and stringent physical constraints. While current deep reinforcement learning (DRL) methods for online 3D-BPP have shown promising results in optimizing average performance over an underlying box sequence distribution, they often fail in real-world settings where some worst-case scenarios can materialize. Standard robust DRL algorithms tend to overly prioritize optimizing the worst-case performance at the expense of performance under normal problem instance distribution. To address these issues, we first introduce a permutation-based attacker to investigate the practical robustness of both DRL-based and heuristic methods proposed for solving online 3D-BPP. Then, we propose an adjustable robust reinforcement learning (AR2L) framework that allows efficient adjustment of robustness weights to achieve the desired balance of the policy's performance in average and worst-case environments. Specifically, we formulate the objective function as a weighted sum of expected and worst-case returns, and derive the lower performance bound by relating to the return under a mixture dynamics. To realize this lower bound, we adopt an iterative procedure that searches for the associated mixture dynamics and improves the corresponding policy. We integrate this procedure into two popular robust adversarial algorithms to develop the exact and approximate AR2L algorithms. Experiments demonstrate that AR2L is versatile in the sense that it improves policy robustness while maintaining an acceptable level of performance for the nominal case.

IROS Conference 2022 Conference Paper

Backward Imitation and Forward Reinforcement Learning via Bi-directional Model Rollouts

• Yuxin Pan
• Fangzhen Lin

Traditional model-based reinforcement learning (RL) methods generate forward rollout traces using the learnt dynamics model to reduce interactions with the real environment. The recent model-based RL method considers the way to learn a backward model that specifies the conditional probability of the previous state given the previous action and the current state to additionally generate backward rollout trajectories. However, in this type of model-based method, the samples derived from backward rollouts and those from forward rollouts are simply aggregated together to optimize the policy via the model-free RL algorithm, which may decrease both the sample efficiency and the convergence rate. This is because such an approach ignores the fact that backward rollout traces are often generated starting from some high-value states and are certainly more instructive for the agent to improve the behavior. In this paper, we propose the backward imitation and forward reinforcement learning (BIFRL) framework where the agent treats backward rollout traces as expert demonstrations for the imitation of excellent behaviors, and then collects forward rollout transitions for policy reinforcement. Consequently, BIFRL empowers the agent to both reach to and explore from high-value states in a more efficient manner, and further reduces the real interactions, making it potentially more suitable for real-robot learning. Moreover, a value-regularized generative adversarial network is introduced to augment the valuable states which are infrequently received by the agent. Theoretically, we provide the condition where BIFRL is superior to the baseline methods. Experimentally, we demonstrate that BIFRL acquires the better sample efficiency and produces the competitive asymptotic performance on various MuJoCo locomotion tasks compared against state-of-the-art model-based methods.

AAAI Conference 2021 Conference Paper

Parameterized Logical Theories

• Fangzhen Lin

A theory in first-order logic is a set of sentences. A parameterized theory is a first-order theory with some of its predicates and functions identified as parameters, together with some import statements that call other parameterized theories. A KB is then a collection of these interconnected parameterized theories, similar to how a computer program is constructed as a set of functions in a modern programming language. In this paper, we provide a translational semantics for these parameterized theories in first-order logic using the situation calculus. We also discuss their potential uses in areas such as multi-context reasoning and logical formalization of computer programs.

AAAI Conference 2020 System Paper

Embedding High-Level Knowledge into DQNs to Learn Faster and More Safely

• Zihang Gao
• Fangzhen Lin
• Yi Zhou
• Hao Zhang
• Kaishun Wu
• Haodi Zhang

Deep reinforcement learning has been successfully applied in many decision making scenarios. However, the slow training process and difficulty in explaining limit its application. In this paper, we attempt to address some of these problems by proposing a framework of Rule-interposing Learning (RIL) that embeds knowledge into deep reinforcement learning. In this framework, the rules dynamically effect the training progress, and accelerate the learning. The embedded knowledge in form of rule not only improves learning efficiency, but also prevents unnecessary or disastrous explorations at early stage of training. Moreover, the modularity of the framework makes it straightforward to transfer high-level knowledge among similar tasks.

AAAI Conference 2020 Conference Paper

Nice Invincible Strategy for the Average-Payoff IPD

• Shiheng Wang
• Fangzhen Lin

The Iterated Prisoner’s Dilemma (IPD) is a well-known benchmark for studying the long term behaviours of rational agents. Many well-known strategies have been studied, from the simple tit-for-tat (TFT) to more involved ones like zero determinant and extortionate strategies studied recently by Press and Dyson. In this paper, we consider what we call invincible strategies. These are ones that will never lose against any other strategy in terms of average payoff in the limit. We provide a simple characterization of this class of strategies, and show that invincible strategies can also be nice. We discuss its relationship with some important strategies and generalize our results to some typical repeated 2x2 games. It’s known that experimentally, nice strategies like the TFT and extortionate ones can act as catalysts for the evolution of cooperation. Our experiments show that this is also the case for some invincible strategies that are neither nice nor extortionate.

AAMAS Conference 2019 Conference Paper

Invincible Strategies of Iterated Prisoner's Dilemma

• Shiheng Wang
• Fangzhen Lin

The Iterated Prisoner’s Dilemma (IPD) is a well-known benchmark for studying rational agents’ long term behaviour such as how cooperation can emerge among selfish and unrelated agents that need to co-exist over long term. Many well-known strategies have been studied, from the simple tit-for-tat (TFT) made famous by Axelrod after his influential tournaments to more involved ones like zero determinant and extortionate strategies studied recently by Press and Dyson. In this paper, we consider what we call invincible strategies. These are ones that will never lose against any other strategy in terms of average payoff in the limit. We provide a simple characterization of this class of strategies, and discuss its relationship with some other classes of strategies.

AIJ Journal 2017 Journal Article

Characterizing causal action theories and their implementations in answer set programming

• Haodi Zhang
• Fangzhen Lin

AAMAS Conference 2017 Conference Paper

K-Memory Strategies in Repeated Games

• Lijie Chen
• Fangzhen Lin
• Pingzhong Tang
• Kangning Wang
• Ruosong Wang
• Shiheng Wang

In this paper, we study k-memory strategies in two-person repeated games. An agent adopting such a strategy makes his decision only based on the action profiles of the previous k rounds. We show that in finitely repeated games, the best response of a k-memory strategy may not even be a constant-memory strategy. However, in infinitely repeated games, one of the best responses against any given k-memory strategy must be k-memory. Our results are enabled by a graph-structural characterization of the best responses of kmemory strategies. We put forward polynomial algorithms to compute best responses.

AIJ Journal 2016 Journal Article

A formalization of programs in first-order logic with a discrete linear order

• Fangzhen Lin

AAAI Conference 2016 Conference Paper

Mapping Action Language BC to Logic Programs: A Characterization by Postulates

• Haodi Zhang
• Fangzhen Lin

We have earlier shown that the standard mappings from action languages B and C to logic programs under answer set semantics can be captured by sets of properties on transition systems. In this paper, we consider action language BC and show that a standard mapping from BC action descriptions to logic programs can be similarly captured when the action rules in the descriptions do not have consistency conditions.

IJCAI Conference 2015 Conference Paper

Characterizing Causal Action Theories and Their Implementations in Answer Set Programming: Action Languages B, C, and Beyond

• Haodi Zhang
• Fangzhen Lin

We consider a simple language for writing causal action theories, and postulate several properties for the state transition models of these theories. We then consider some possible embeddings of these causal action theories in some other action formalisms, and their implementations in logic programs with answer set semantics. In particular, we propose to consider what we call permissible translations from these causal action theories to logic programs. We identify two sets of properties, and prove that for each set, there is only one permissible translation, under strong equivalence, that can satisfy all properties in the set. As it turns out, for one set, the unique permissible translation is essentially the same as Balduccini and Gelfond’s translation from Gelfond and Lifschitz’s action language B to logic programs. For the other, it is essentially the same as Lifschitz and Turner’s translation from the action language C to logic programs. This work provides a new perspective on understanding, evaluating and comparing action languages by using sets of properties instead of examples. It will be interesting to see if other action languages can be similarly characterized, and whether new action formalisms can be defined using different sets of properties.

KR Conference 2014 Conference Paper

A First-Order Semantics for Golog and ConGolog

• Fangzhen Lin

KR Conference 2014 Conference Paper

A Formalization of Programs in First-Order Logic with a Discrete Linear Order

• Fangzhen Lin

may want to prove about the program. For instance, trivially, the following assignment We consider the problem of representing and reasoning about computer programs, and propose a translator from a core procedural iterative programming language to first-order logic with quantification over the domain of natural numbers that includes the usual successor function and the “less than” linear order, essentially a first-order logic with a discrete linear order. Unlike Hoare’s logic, our approach does not rely on loop invariants. Unlike typical temporal logic specification of a program, our translation does not require a transition system model of the program, and is compositional on the structures of the program. Some non-trivial examples are given to show the effectiveness of our translation for proving properties of programs. X = X+Y can be captured by the following two axioms: X 0 = X + Y, Y 0 = Y, where X and Y denote the initial values of the corresponding program variables and X 0 and Y 0 their values after the statement is performed. Obviously, the question is how the same can be done for loops. This is where quantification over natural numbers come in. Consider the following while loop

AAAI Conference 2014 Conference Paper

On Computing Optimal Strategies in Open List Proportional Representation: The Two Parties Case

• Ning Ding
• Fangzhen Lin

Open list proportional representation is an election mechanism used in many elections, including the 2012 Hong Kong Legislative Council Geographical Constituencies election. In this paper, we assume that there are just two parties in the election, and that the number of votes that a list would get is the sum of the numbers of votes that the candidates in the list would get if each of them would go alone in the election. Under these assumptions, we formulate the election as a mostly zero-sum game, and show that while the game always has a pure Nash equilibrium, it is NP-hard to compute it.

AAMAS Conference 2013 Conference Paper

Voting with Partial Information: What Questions to Ask?

• Ning Ding
• Fangzhen Lin

Voting is a way to aggregate individual voters’ preferences. Traditionally a voter’s preference is represented by a total order on the set of candidates. However, sometimes one may not have complete information about a voter’s preference, and in this case, can only model a voter’s preference as a partial order. Given this framework, there has been work on computing the possible and necessary winners of a (partial) profile. In this paper, we take a step further, look at sets of questions to ask in order to determine the outcome of such a partial profile. Specifically, we call a set of questions a deciding set for a candidate if the outcome of the vote for the candidate is determined no matter how the questions are answered by the voters, and a possible winning (losing) set if there is a way to answer these questions to make the candidate a winner (loser) of the vote. We discuss some interesting properties about these sets of queries, prove some complexity results about them under some well-known voting rules such as plurality and Borda, and consider their application in vote elicitation.

AAAI Conference 2012 Conference Paper

A Well-Founded Semantics for Basic Logic Programs with Arbitrary Abstract Constraint Atoms

• Yisong Wang
• Fangzhen Lin
• Mingyi Zhang
• Jia-Huai You

Logic programs with abstract constraint atoms proposed by Marek and Truszczynski are very general logic programs. They are general enough to capture aggregate logic programs as well as recently proposed description logic programs. In this paper, we propose a wellfounded semantics for basic logic programs with arbitrary abstract constraint atoms, which are sets of rules whose heads have exactly one atom. We show that similar to the well-founded semantics of normal logic programs, it has many desirable properties such as that it can be computed in polynomial time, and is always correct with respect to the answer set semantics. This paves the way for using our well-founded semantics to simplify these logic programs. We also show how our semantics can be applied to aggregate logic programs and description logic programs, and compare it to the wellfounded semantics already proposed for these logic programs.

AIJ Journal 2012 Journal Article

Ordered completion for first-order logic programs on finite structures

• Vernon Asuncion
• Fangzhen Lin
• Yan Zhang
• Yi Zhou

AAAI Conference 2011 Conference Paper

Causal Theories of Actions Revisited

• Fangzhen Lin
• Mikhail Soutchanski

It has been argued that causal rules are necessary for representing both implicit side-effects of actions and action quali- fications, and there have been a number different approaches for representing causal rules in the area of formal theories of actions. These different approaches in general agree on rules without cycles. However, they differ on causal rules with mutual cyclic dependencies, both in terms of how these rules are supposed to be represented and their semantics. In this paper we show that by adding one more minimization to Lin’s circumscriptive causal theory in the situation calculus, we can have a uniform representation of causal rules including those with cyclic dependencies. We also demonstrate that sometimes causal rules can be compiled into logically equivalent (under a proposed semantics) successor state axioms even in the presence of cyclical dependencies between fluents.

AIJ Journal 2011 Journal Article

Discovering theorems in game theory: Two-person games with unique pure Nash equilibrium payoffs

• Pingzhong Tang
• Fangzhen Lin

AIJ Journal 2011 Journal Article

From answer set logic programming to circumscription via logic of GK

• Fangzhen Lin
• Yi Zhou

AIJ Journal 2011 Journal Article

Loop-separable programs and their first-order definability

• Yin Chen
• Fangzhen Lin
• Yan Zhang
• Yi Zhou

AIJ Journal 2010 Journal Article

Designing competitions between teams of individuals

• Pingzhong Tang
• Yoav Shoham
• Fangzhen Lin

AAAI Conference 2010 Conference Paper

Ordered Completion for First-Order Logic Programs on Finite Structures

• Vernon Asuncion
• Fangzhen Lin
• Yan Zhang
• Yi Zhou

In this paper, we propose a translation from normal first-order logic programs under the answer set semantics to first-order theories on finite structures. Specifically, we introduce ordered completions which are modifications of Clark’s completions with some extra predicates added to keep track of the derivation order, and show that on finite structures, classical models of the ordered-completion of a normal logic program correspond exactly to the answer sets (stable models) of the logic program.

IJCAI Conference 2009 Conference Paper

• Pingzhong Tang
• Fangzhen Lin

In this paper we provide a logical framework for using computers to discover theorems in two-person finite games in strategic form, and apply it to discover classes of games that have unique pure Nash equilibrium payoffs. We consider all possible classes of games that can be expressed by a conjunction of two binary clauses, and our program rediscovered Kats and Thisse’s class of weakly unilaterally competitive two-person games, and came up with several other classes of games that have unique pure Nash equilibrium payoffs. It also came up with new classes of strict games that have unique pure Nash equilibria, where a game is strict if for both player different profiles have different payoffs.

AIJ Journal 2009 Journal Article

Computer-aided proofs of Arrow's and other impossibility theorems

• Pingzhong Tang
• Fangzhen Lin

AAMAS Conference 2009 Conference Paper

Team Competition

• Pingzhong Tang
• Yoav Shoham
• Fangzhen Lin

In a team competition, two participating teams have an equal number of players, and each team orders its players linearly based on their strengths. A mechanism then specifies how the players from the two teams are matched up and how to score them. There are two types of manipulations by a team: Misreporting the strength ordering and deliberately losing a match. To identify these strategically behaviors, we model the team competition problem in a game-theoretical framework, under which we prove necessary and sufficient conditions which ensure that truthful reporting and maximal effort in matches are equilibrium strategies, and which further ensure certain fairness conditions described by choice functions.

AAAI Conference 2008 Conference Paper

Abductive Logic Programming by Nonground Rewrite Systems

• Fangzhen Lin

Logic programming with negation offers a compelling approach to abductive reasoning. This paper shows a simple view of abduction in this context for the completion semantics, under which the problem of abduction becomes one of solving quantified equations and disequations. By this way of treating abduction, the problems with nonground negative queries in the previous approaches no longer exist. We show the soundness and completeness results for our approach.

KR Conference 2008 Conference Paper

Answer Set Programming with Functions

• Fangzhen Lin
• Yisong Wang

To compute a function such as a mapping from vertices to colors in the graph coloring problem, current practice in Answer Set Programming is to represent the function as a relation. Among other things, this often makes the resulting program unnecessarily large when instantiated on a large domain. The extra constraints needed to enforce the relation as a function also make the logic program less transparent. In this paper, we consider adding functions directly to normal logic programs. We show that the answer set semantics can be generalized to these programs straightforwardly. We also show that the notions of loops and loop formulas can be extended, and that through program completion and loop formulas, a normal logic program with functions can be transformed to a Constraint Satisfaction problem.

AAAI Conference 2008 Conference Paper

Computer-Aided Proofs of Arrow’s and Other Impossibility Theorems

• Fangzhen Lin

Arrow’s Impossibility Theorem is one of the landmark results in social choice theory. Over the years since the theorem was proved in 1950, quite a few alternative proofs have been put forward. In this paper, we propose yet another alternative proof of the theorem. The basic idea is to use induction to reduce the theorem to the base case with 3 alternatives and 2 agents and then use computers to verify the base case. This turns out to be an effective approach for proving other impossibility theorems such as Sen’s and Muller-Satterthwaite’s theorems as well. Furthermore, we believe this new proof opens an exciting prospect of using computers to discover similar impossibility or even possibility results.

KR Conference 2008 Conference Paper

Computing Loops with at Most One External Support Rule

• Xiaoping Chen
• Jianmin Ji
• Fangzhen Lin

If a loop has no external support rules, then its loop formula is equivalent to a set of unit clauses; and if it has exactly one external support rule, then its loop formula is equivalent to a set of binary clauses. In this paper, we consider how to compute these loops and their loop formulas in a normal logic program, and use them to derive consequences of a logic program. We show that an iterative procedure based on unit propagation, the program completion and the loop formulas of loops with no external support rules can compute the same consequences as the "Expand" operator in smodels, which is known to compute the well-founded model when the given normal logic program has no constraints. We also show that using the loop formulas of loops with at most one external support rule, the same procedure can compute more consequences, and these extra consequences can help ASP solvers such as cmodels to find answer sets of certain logic programs.

KR Conference 2008 Conference Paper

Proving Goal Achievability

• Fangzhen Lin

Given an action theory, a goal, and a set of initial states, we consider the problem of checking whether the goal is always achievable in every initial state of the set. To address this problem, we introduce a notion of reduction between sets of states, and show that if the set of the initial states can be reduced to one of its subsets, then the problem is equivalent to checking whether the goal is achievable in every initial state of the subset, provided that all the variables in the goal, if any, are existentially quantified, and that the preconditions and effects of the actions can be specified by quantifier-free formulas. We believe that this result provides an effective way of proving goal achievability, and illustrate it through some examples.

IJCAI Conference 2007 Conference Paper

• Fangzhen Lin
• Yi Zhou

We first provide a mapping from Pearce's equilibrium logic and Ferraris and Lifschitz's general logic programs to Lin and Shoham's logic of knowledge and justified assumptions, a nonmonotonic modal logic that has been shown to include as special cases both Reiter's default logic in the propositional case and Moore's autoepistemic logic. From this mapping, we obtain a mapping from general logic programs to circumscription, both in the propositional and first-order case. Furthermore, we show that this mapping can be used to check the strong equivalence between two propositional logic programs in classical logic.

KR Conference 2006 Conference Paper

First-Order Loop Formulas for Normal Logic Programs

• Fangzhen Lin
• Yin Chen
• Yisong Wang
• Mingyi Zhang

In this paper we extend Lin and Zhao's notions of loops and loop formulas to normal logic programs that may contain variables. Under our definition, a loop formula of such a logic program is a first-order sentence. We show that together with Clark's completion, our notion of first-order loop formulas captures the answer set semantics on the instantiation-basis: for any finite set F of ground facts about the extensional relations of a program P, the answer sets of the ground program obtained by instantiating P using F are exactly the models of the propositional theory obtained by instantiating using F the first order theory consisting of the loop formulas of P and Clark's completion of the union of P and F. We also prove a theorem about how to check whether a normal logic program with variables has only a finite number of non-equivalent first-order loops.

AIJ Journal 2006 Journal Article

Loop formulas for circumscription

• Joohyung Lee
• Fangzhen Lin

IJCAI Conference 2005 Conference Paper

Discovering Classes of Strongly Equivalent Logic Programs

• Fangzhen Lin
• Yin

We report on a successful experiment of computeraided theorem discovery in the area of logic programming with answer set semantics. Specifically, with the help of computers, we discovered exact conditions that capture the strong equivalence between a set of a rule and the empty set, a set of a rule and another set of a rule, a set S of two rules and a subset of S with one rule, a set of two rules and a set of another rule, and a set S of three rules and a subset of S with two rules. We prove some general theorems that can help us verify the correctness of these conditions, and discuss the usefulness of our results in program simplification.

AIJ Journal 2004 Journal Article

ASSAT: computing answer sets of a logic program by SAT solvers

• Fangzhen Lin
• Yuting Zhao

KR Conference 2004 Conference Paper

Discovering State Invariants

• Fangzhen Lin

We continue to advocate a methodology that we used earlier for pattern discovery through exhaustive search in selected small domains. This time we apply it to the problem of discovering state invariants in planning domains. State invariants are formulas that if true in a state, will be true in all successor states. In this paper, we consider the following four types of state invariants commonly found in AI planning domains: functional dependency constraints, constraints on mutual exclusiveness of categories, type information constraints, and domain closure axioms. As it turned out, for a class of action theories that include many planning benchmarks, for the first three types of constraints, whether they are state invariants can be verified by considering models whose domains are bounded by a small finite number. This forms the basis for a procedure that tries to discover state invariants by exhaustive search in small finite domains. An implementation of the procedure yields encouraging results in the blocks world and the logistics domain.

AAAI Conference 2004 Conference Paper

Loop Formulas for Circumscription

• Joohyung Lee
• Fangzhen Lin

Clark’s completion is a simple nonmonotonic formalism and a special case of many nonmonotonic logics. Recently there has been work on extending completion with “loop formulas” so that general cases of nonmonotonic logics such as logic programs (under the answer set semantics) and McCain–Turner causal logic can be characterized by propositional logic in the form of “completion + loop formulas”. In this paper, we show that the idea is applicable to McCarthy’s circumscription in the propositional case. We also show how to embed propositional circumscription in logic programs and in causal logic, inspired by the uniform characterization of “completion + loop formulas”.

AAAI Conference 2004 Conference Paper

On Odd and Even Cycles in Normal Logic Programs

• Fangzhen Lin
• Xishun Zhao

An odd cycle of a logic program is a simple cycle that has an odd number of negative edges in the dependency graph of the program. Similarly, an even cycle is one that has an even number of negative edges. For a normal logic program that has no odd cycles, while it is known that such a program always has a stable model, and such a stable model can be computed in polynomial time, we show in this paper that checking whether an atom is in a stable model is NP-complete, and checking whether an atom is in all stable models is co-NP complete, both are the same as in the general case for normal logic programs. Furthermore, we show that if a normal logic program has exactly one odd cycle, then checking whether it has a stable model is NP-complete, again the same as in the general case. For normal logic programs with a fixed number of even cycles, we show that there is a polynomial time algorithm for computing all stable models. Furthermore, this polynomial time algorithm can be improved significantly if the number of odd cycles is also fixed.

IJCAI Conference 2003 Conference Paper

Causal Theories of Action: A Computational Core

• Jerome Lang
• Fangzhen Lin
• Pierre Marquis

We propose a framework for simple causal theories of action, and study the computational complexity in it of various reasoning tasks such as determinism, progression and regression under various assumptions. As it turned out, even the simplest one among them, one-step temporal projection with complete initial state, is intractable. We also briefly consider an extension of the framework to allow truly indeterministic actions, and find that this extension does not increase the complexity of any of the tasks considered here.

IJCAI Conference 2003 Conference Paper

Recycling Computed Answers in Rewrite Systems for Abduction

• Fangzhen Lin
• Jia-Huai You

In rule-based systems, goal-oriented computations correspond naturally to the possible ways that an observation may be explained. In some applications, we need to compute explanations for a series of observations with the same domain. The question whether previously computed answers can be recycled arises. A yes answer could result in substantial savings of repeated computations. For systems based on classic logic, the answer is yes. For nonmonotonic systems however, one tends to believe that the answer should be no, since recycling is a form of adding information. In this paper, we show that computed answers can always be recycled, in a nontrivial way, for the class of rewrite procedures proposed earlier in [Lin and You, 2001] for logic programs with negation. We present some experimental results on an encoding of a logistics domain.

AIJ Journal 2002 Journal Article

Abduction in logic programming: A new definition and an abductive procedure based on rewriting

• Fangzhen Lin
• Jia-Huai You

KR Conference 2002 Conference Paper

Reducing strong equivalence of logic programs to entailment in classical propositional logic

• Fangzhen Lin

AIJ Journal 2001 Journal Article

On strongest necessary and weakest sufficient conditions☆☆An earlier version of this paper was the co-winner of the Best Paper Award at KR2000.

• Fangzhen Lin

AAAI Conference 2000 Conference Paper

From Causal Theories to Successor State Axioms and STRIPS-Like Systems

• Fangzhen Lin

We describe a system for specifying the effects of actions. Unlike those commonly used in AI planning, our system uses an action description language that allows one to specify the effects of actions using domain rules, which are state constraints that can entail new action effects from old ones. Declaratively, an action domain in our language corresponds to a nonmonotonic causal theory in the situation calculus. Procedurally, such an action domain is compiled into a set of propositional theories, one for each action in the domain, from which fully instantiated successor state-like axioms and STRIPS-like systems are then generated. We expect the system to be a useful tool for knowledge engineers writing action specifications for classical AI planning systems, GOLOG systems, and other systems where formal specifications of actions are needed.

AIJ Journal 1998 Journal Article

Applications of the situation calculus to formalizing control and strategic information: the Prolog cut operator

• Fangzhen Lin

AIJ Journal 1998 Journal Article

What robots can do: robot programs and effective achievability

• Fangzhen Lin
• Hector J. Levesque

IJCAI Conference 1997 Conference Paper

Applications of the Situation Calculus To Formalizing Control and Strategic Information: The Prolog Cut Operator

• Fangzhen Lin

We argue that the situation calculus is a natural formalism for representing and reasoning about control and strategic information. As a case study, in this paper we provide a situation calculus semantics for the Prolog cut operator, the central search control operator in Prolog. We show that our semantics is well-behaved when the programs are properly stratified. We also show that according to this semantics, the conventional implementation of the negationas-failure operator using cut is provably correct with respect to the stable model semantics.

AIJ Journal 1997 Journal Article

How to progress a database

• Fangzhen Lin
• Ray Reiter

AAAI Conference 1996 Conference Paper

Embracing Causality in Specifying the Indeterminate Effects of Actions

• Fangzhen Lin

This paper makes the following two contributions to formal theories of actions: Showing that a causal minimization framework can be used effectively to specify the effects of indeterminate actions; and showing that for certain classes of such actions, regression, an effective computational mechanism, can be used to reason about them. Logical Preliminaries We shall investigate the problem in the framework of the situation calculus [8]. Our version of it employs a many sorted second-order language. We assume the following sorts: situation for situations, action for actions, fluent for propositional fluents, truth-value for truth values true and false, and object for everything else. We use the following domain independent predicates and functions:

IJCAI Conference 1995 Conference Paper

Embracing Causality in Specifying the Indirect Effects of Actions

• Fangzhen Lin

IJCAI Conference 1995 Conference Paper

How to Progress a Database 11 The STRIPS Connection

• Fangzhen Lin
• Ray Reiter

AIJ Journal 1992 Journal Article

A logic of knowledge and justified assumptions

• Fangzhen Lin
• Yoav Shoham

AAAI Conference 1992 Conference Paper

Concurrent Actions in the Situation Calculus

• Fangzhen Lin

We propose a representation of concurrent actions; rather than invent a new formalism, we model them within the standard situation calculus by introducing the notions of global actions and primitive actions, whose relationship is analogous to that between situations and fluents. The result is a framework in which situations and actions play quite symmetric roles. The rich structure of actions gives rise to a new problem, which, due to this symmetry between actions and situations, is analogous to the traditional frame problem. In [Lin and Shoham 19911 we provided a solution to the frame problem based on a formal adequacy criterion called “ epistemological completeness. ” Here we show how to solve the new problem based on the same adequacy criterion,

AAAI Conference 1991 Conference Paper

Provably Correct Theories of Action (Preliminary Report)

• Fangzhen Lin

TARK Conference 1990 Conference Paper

Epistemic Semantics for Fixed-Points Non-Monotonic Logics

• Fangzhen Lin
• Yoav Shoham

Default Logic and Autoepistemic Logic are the two best-known fixed-points nonmonotonic logics. Despite the fact that they are known to be closely related and that the epistemic nature of Autoepistemic Logic is obvious, the only semantics that have been offered for Default Logic to date are complex and have little to do with epistemic notions [Etherington 1987]. In this paper we provide simple uniform epistemic semantics for the two logics. We do so by translating them both into a new logic, called GK, of Grounded Knowledge, which embodies a modification of preference semantics [Shoham 1987]. Beside their simplicity and uniformity, the semantics have two other advantages: They allow easy proofs of the connections between Default Logic and Autoepistemic Logic, and suggest a general class of logics of which the two logics are special cases.

TARK Conference 1988 Conference Paper

Circumscription in a Modal Logic

• Fangzhen Lin

In this paper, we extend circumscription [McCarthy, 80] to a propositional modal logic of knowledge of one agent. Instead of circumscribing a predicate, we circumscribe the knowledge operator "K" in a formula. In order to have a nontrivial circumscription schema, we extend $5 modal logic of knowledge by adding another modality "Val" and a universal quantifier over base sentences (sentences which do not contain modality). Intuitively, "Val(P)" means that P is a valid formula. It turns out that by circumscribing the knowledge operator in a formula, we completely characterize the maximally ignorant models of the formula (models of the formula where agents have minimal knowledge).

AAAI Conference 1987 Conference Paper

Reasoning in the Presence of Inconsistency

• Fangzhen Lin

In this paper, we propose a logic which is nontrivial in the presence of inconsistency. The logic is based on the resolution principle and coincides with the classical logic when premises are consistent. Some results of interesting to Automated Theorem Proving are a sound and sometimes complete three-valued semantics for the resolution rule and a refutation process which is much in the spirit of the problem reduction format.