期刊
ARTIFICIAL INTELLIGENCE
卷 162, 期 1-2, 页码 49-88出版社
ELSEVIER
DOI: 10.1016/j.artint.2004.11.004
关键词
reasoning with structure; theorem proving; first-order logic; SAT; tree decomposition; graphical models; parallel computation; distributed computation
In this paper we show how tree decomposition can be applied to reasoning with first-order and propositional logic theories. Our motivation is two-fold. First, we are concerned with how to reason effectively with multiple knowledge bases that have overlap in content. Second, we are concerned with improving the efficiency of reasoning over a set of logical axioms by partitioning the set with respect to some detectable structure, and reasoning over individual partitions either locally or in a distributed fashion. To this end, we provide algorithms for partitioning and reasoning with related logical axioms in propositional and first-order logic. Many of the reasoning algorithms we present are based on the idea of passing messages between partitions. We present algorithms for both forward (data-driven) and backward (query-driven) message passing. Different partitions may have different associated reasoning procedures. We characterize a class of reasoning procedures that ensures completeness and soundness of our message-passing algorithms. We further provide a specialized algorithm for propositional satisfiability checking with partitions. Craig's interpolation theorem serves as a key to proving soundness and completeness of all of these algorithms. An analysis of these algorithms emphasizes parameters of the partitionings that influence the efficiency of computation. We provide a greedy algorithm that automatically decomposes a set of logical axioms into partitions, following this analysis. (C) 2004 Published by Elsevier B.V.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据