Results on Reasoning about Updates in Transaction Logic
Results on Reasoning about Updates in Transaction Logic
复制标题
关于事务逻辑更新的推理结果
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
M. Kifer
中科院分区：
文献类型：
--
作者：
A. Bonner;M. Kifer
事务逻辑被设计为演绎数据库和逻辑程序状态变化的一般逻辑。它有一个模型理论，一个证明理论，它的霍恩子集可以给出一个程序解释。先前的研究表明，声明性语义和过程解释的结合将事务逻辑的Horn子集变成了一种强大的具有更新的逻辑编程语言[BK98，BK94,BK93,BK95]。在本文中，我们关注的不是Horn子集，而是完整的逻辑，并且我们探索了它作为一种对具有更新的逻辑程序进行推理的形式主义的潜力。我们首先开发了一种方法来指定这类程序的属性，然后提供了一个合理的推理系统来对它们进行推理，并推测了一个完备性结果。最后，我们通过一系列增加难度的例子来说明推理系统的能力。
Transaction Logic was designed as a general logic of state change for deductive databases and logic programs. It has a model theory, a proof theory, and its Horn subset can be given a procedural interpretation. Previous work has demonstrated that the combination of declarative semantics and procedural interpretation turns the Horn subset of Transaction Logic into a powerful language for logic programming with updates [BK98,BK94,BK93,BK95]. In this paper, we focus not on the Horn subset, but on the full logic, and we explore its potential as a formalism for reasoning about logic programs with updates. We first develop a methodology for specifying properties of such programs, and then provide a sound inference system for reasoning about them, and conjecture a completeness result. Finally, we illustrate the power of the inference system through a series of examples of increasing difficulty.