Loading...
Please wait, while we are loading the content...
Similar Documents
Partition-Based Logical Reasoning for First-Order and Propositional Theories
| Content Provider | CiteSeerX |
|---|---|
| Author | Eyal Amir, A. Sheila Mcilraith, B. |
| Abstract | In this paper we provide algorithms for reasoning with partitions of related logical axioms in propositional and first-order logic (FOL). We also provide a greedy algorithm that automatically decomposes a set of logical axioms into partitions. 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. Many of the reasoning procedures we present are based on the idea of passing messages between partitions. We present algorithms for reasoning using forward (data driven) message-passing and using backward (query driven) message-passing with partitions of logical axioms. Associated with each partition is a reasoning procedure. We characterize a class of reasoning procedures that ensures completeness and soundness of our message-passing algorithms. We also provide a specialized algorithm for propositional satisfiability checking with partitions. Craig’s interpolation theorem serves as a key to proving soundness and completeness of these algorithms. An analysis of these algorithms emphasizes parameters of partitionings that influence the efficiency of computation. These parameters are the number of symbols shared by a pair of partitions, the size (number of symbols) of each partition, and the topology of the partitioning. We provide a principled way for automatically decomposing a given theory into partitions. We provide a greedy algorithm that instantiates this method while exploiting the parameters that influence the efficiency of computation. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Logical Axiom Partition-based Logical Reasoning Propositional Theory Greedy Algorithm Detectable Structure Craig Interpolation Theorem Message-passing Algorithm Multiple Knowledge Base Principled Way Reasoning Procedure Specialized Algorithm Present Algorithm Related Logical Axiom Individual Partition Propositional Satisfiability First-order Logic |
| Content Type | Text |
| Resource Type | Article |
