Transaction Logic: Unifying Declarative and Procedural Knowledge - Extended Abstract -
Anthony J. Bonner, Michael Kifer · 1993
This paper presents AI applications of recently proposed Transaction Logic (abbr., 7-7z) [2]. Transaction Logic is a novel formalism that accounts in a clean and declarative fashion for phenomenon of updating first-order knowledge bases, most notably, databases and logic programs. Transaction Logic has a natural model theory and a sound-and-complete proof theory. Unlike many other logics, Tn allows users to program transactions that modify state of a knowledge base. This is possible because, like classical logic, Tn has a Horn version which has both a procedural and a declarative semantics, as well as an efficient SLD-style proof procedure. As a result, Tn is a unifying, logical formalism for specifying both declarative and procedural knowledge. Furthermore, for a wide range of practical problems, frame problem [18] is not an issue for /-n. This is because Tn performs real updates on materialized databases, much as procedural languages like Pascal do. A key contribution of ~-n is capturing these procedural updates in a logical framework with an efficient proof theory. A full development of proof theory, a discussion of frame problem, and applications to database systems can be found in [2, 3]. This paper presents model theory of 7-~¢, and then focuses on applications of Tn to problems in AI, especially planning, temporal reasoning, constraint satisfaction, hypothetical and counterfactual reasoning, and representation and use of procedural knowledge. The importance of procedural knowledge has been extensively argued in AI literature (see e.g., [8]). For instance, well-known SHRDLU program [26] is largely based on procedural knowledge. In fact, Winograd argues in [26] that procedural knowledge is inherent in automated natural language understanding. For example, meaning of the is a collection of procedures