Minimal founded semantics for disjunctive logic programs and deductive databases

论Datalog$^\ eg$的布尔网络理论

On the Boolean Network Theory of Datalog$^\neg$

该研究建立Datalog$^\ eg$与布尔网络理论的形式关联，证明不同环结构下模型的等价性、存在性与唯一性，给出模型数量上界，并揭示子集极小稳定陷阱空间与正则模型的等价关系。

析取存在规则的有限公理化

Finite Axiomatizability by Disjunctive Existential Rules

本文通过临界性、直积封闭性和新提出的图解兼容性等模型论性质，刻画了析取存在规则有限公理化的充要条件，并将其推广到线性与受保护规则类，用于规则改写。

Semantical Characterizations and Complexity of Equivalences in Answer Set Programming

In recent research on non-monotonic logic programming, repeatedly strong equivalence of logic programs P and Q has been considered, which holds if the programs P union R and Q union R have the same answer sets for any other program R. This property strengthens equivalence of P and Q with respect to answer sets (which is the particular case for R is the empty set), and has its applications in program optimization, verification, and modular logic programming. In this paper, we consider more liberal notions of strong equivalence, in which the actual form of R may be syntactically restricted. On t…

Automated Mutual Explicit Induction Proof in Separation Logic

We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit induction proof, is an instance of Noetherian induction. Specifically, we propose a novel induction principle on a well-founded relation of separation logic model and follow the explicit induction methods to implement this principle as inference rules, so that it can be easily integrated into a deductive system. We also support mutual induction, a natural feature of implicit induction, where the goal entailment and other en…