# zbMATH — the first resource for mathematics

Partition-based logical reasoning for first-order and propositional theories. (English) Zbl 1132.68672
Summary: 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.

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68P15 Database theory
##### Software:
BREAKUP; GETFOL; SPTHEO
Full Text:
##### References:
 [1] Ahuja, R.K.; Orlin, J.B., Distance directed augmenting path algorithms for maximum flow and parametric maximum flow problems, Naval research logistics quarterly, 38, 413-430, (1991) · Zbl 0724.90021 [2] Akman, V.; Surav, M., Steps toward formalizing context, AI magazine, 17, 3, 55-72, (1996) [3] Amir, E., (de)composition of situation calculus theories, (), 456-463 [4] Amir, E., Efficient approximation for triangulation of minimum treewidth, (), 7-15 [5] Amir, E.; McIlraith, S., Partition-based logical reasoning, (), 389-400 [6] E. Amir, S. McIlraith, Strategies for focusing structure-based theorem proving, Artificial Intelligence, in press · Zbl 0990.90558 [7] Arnborg, S., Efficient algorithms for combinatorial problems on graphs with bounded decomposability—a survey, Bit, 25, 2-23, (1985) · Zbl 0573.68018 [8] Baader, F.; Schulz, K.U., Unification in the union of disjoint equational theories: combining decision procedures, (), 50-65 · Zbl 0925.03084 [9] Becker, A.; Bar-Yehuda, R.; Geiger, D., Randomized algorithms for the loop cutset problem, J. artificial intelligence res., 12, 219-234, (2000) · Zbl 0947.68138 [10] Becker, A.; Geiger, D., Approximate algorithms for the loop cutset problem, (), 60-68 [11] Becker, A.; Geiger, D., A sufficiently fast algorithm for finding close to optimal junction trees, (), 81-89 [12] Bertele, U.; Brioschi, F., Nonserial dynamic programming, (1972), Academic Press New York · Zbl 0187.17801 [13] W.W. Bledsoe, A.M. Ballantyne, Unskolemizing, Technical Report Memo ATP-41, Mathematics Department, University of Texas, Austin, 1978 [14] Bonacina, M.P.; Hsiang, J., Parallelization of deduction strategies: an analytical study, J. automat. reason., 13, 1-33, (1994) [15] Bonacina, M.P.; Hsiang, J., On the representation of dynamic search spaces in theorem proving, (), 85-94 [16] Bonzon, P.E., A reflective proof system for reasoning in contexts, (), 398-403 [17] Boppana, R.B.; Sipser, M., The complexity of finite functions, (), 757-804 · Zbl 0900.68268 [18] Bossu, G.; Siegel, P., Saturation, nonmonotonic reasoning and the closed world assumption, Artificial intelligence, 25, 1, 13-65, (1985) · Zbl 0569.68078 [19] R.S. Boyer, Locking: a restriction of resolution, PhD thesis, Mathematics Department, University of Texas, Austin, 1971 [20] Carbone, A., Interpolants, cut elimination and flow graphs for the propositional calculus, Ann. pure appl. logic, 83, 3, 249-299, (1997) · Zbl 0873.03050 [21] Chadha, R.; Plaisted, D.A., Finding logical consequences using unskolemization, (), 255-264 [22] Chang, C.-L.; Lee, R.C.-T., Symbolic logic and mechanical theorem proving, (1973), Academic Press New York · Zbl 0263.68046 [23] Chekassky, B.V.; Goldberg, A.V., On implementing the push-relabel method for the maximum flow problem, Algorithmica, 19, 4, 390-410, (1997) · Zbl 0898.68029 [24] Cohen, P.; Schrag, R.; Jones, E.; Pease, A.; Lin, A.; Starr, B.; Gunning, D.; Burke, M., The DARPA high-performance knowledge bases project, AI magazine, 19, 4, 25-49, (1998) [25] Conry, S.E.; McIntosh, D.J.; Meyer, R.A., DARES: a distributed automated reasoning system, (), 78-85 [26] Cook, S.A.; Mitchell, D.G., Finding hard instances of the satisfiability problem: a survey, () · Zbl 0889.68073 [27] Cormen, T.H.; Leiserson, C.E.; Rivest, R.L., Introduction to algorithms, (1989), McGraw Hill New York [28] Cowen, R.; Wyatt, K., BREAKUP: a preprocessing algorithm for satisfiability testing of CNF formulas, Notre dame J. formal logic, 34, 4, 602-606, (1993) · Zbl 0795.03018 [29] Cox, P.; Pietrzykowski, T., A complete nonredundant algorithm for reversed skolemization, Theoret. comput. sci., 28, 239-261, (1984) · Zbl 0566.03005 [30] Craig, W., Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. symbolic logic, 22, 250-268, (1957) · Zbl 0081.24402 [31] Craig, W., Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, J. symbolic logic, 22, 269-285, (1957) · Zbl 0079.24502 [32] Dantzig, G.B.; Fulkerson, D.R., On the MAX-flow MIN-cut theorem of networks, (), 215-221 · Zbl 0072.37802 [33] Darwiche, A., Utilizing knowledge-based semantics in graph-based algorithms, (), 607-613 [34] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Comm. ACM, 5, 394-397, (1962) · Zbl 0217.54002 [35] Dechter, R., Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition, Artificial intelligence, 41, 3, 273-312, (1990) [36] Dechter, R.; El Fattah, Y., Topological parameters for time-space tradeoff, Artificial intelligence, 125, 1, 93, (2001) · Zbl 0969.68149 [37] Dechter, R.; Pearl, J., Tree clustering for constraint networks, Artificial intelligence, 38, 353-366, (1989) · Zbl 0665.68084 [38] Dechter, R.; Rish, I., Directional resolution: the Davis-Putnam procedure, revisited, (), 134-145 [39] del Val, A., A new method for consequence finding and compilation in restricted language, (), 259-264 [40] Denzinger, J.; Fuchs, D., Cooperation of heterogeneous provers, (), 10-15 [41] Denzinger, J., Knowledge-based distributed search using teamwork, (), 81-88 [42] Denzinger, J.; Dahn, I., Cooperating theorem provers, (), 383-416 · Zbl 0970.68157 [43] Denzinger, J.; Fuchs, M.; Fuchs, M., High performance ATP systems by combining several AI methods, (), 102-107 [44] Dinic, E.A., Algorithm for solution of a problem of maximum flow in networks with power estimation, Soviet math. dokl., 11, 1277-1280, (1970) · Zbl 0219.90046 [45] Eisinger, N.; Ohlbach, H.J., Deduction systems based on resolution, () [46] Ertel, W., OR-parallel theorem proving with random competition, (), 226-237 [47] Even, S., An algorithm for determining whether the connectivity of a graph is at least k, SIAM J. comput., 4, 3, 393-396, (1975) · Zbl 0311.05133 [48] Even, S., Graph algorithms, (1979), Computer Science Press · Zbl 0441.68072 [49] Even, S.; Endre Tarjan, R., Network flow and testing graph connectivity, SIAM J. comput., 4, 4, 507-518, (1975) · Zbl 0328.90031 [50] Feige, U.; Krauthgamer, R., A polylogarithmic approximation of the minimum bisection, () · Zbl 1088.05068 [51] Fikes, R.; Farquhar, A., Large-scale repositories of highly expressive reusable knowledge, IEEE intelligent systems, 14, 2, (1999) [52] J.J. Finger, M.R. Genesereth, Residue: a deductive approach to design synthesis, Technical Report STAN-CS-85-1035, Stanford University, Computer Science Department, Stanford, CA, 1985 [53] Ford, L.R.; Fulkerson, D.R., Flows in networks, (1962), Princeton University Press Princeton, NJ · Zbl 0139.13701 [54] Genesereth, M.R.; Nilsson, N.J., Logical foundations of artificial intelligence, (1987), Morgan Kaufmann San Mateo, CA · Zbl 0645.68104 [55] Giunchiglia, E.; Traverso, P., A multi-context architecture for formalizing complex reasoning, Internat. J. intelligent systems, 10, 501-539, (1995), Also, IRST Tech. Report #9307-26 · Zbl 0826.68111 [56] Giunchiglia, F., GETFOL manual—GETFOL version 2.0, technical report DIST-TR-92-0010, DIST—university of Genoa, 1994, and website at [57] Goldberg, A.V.; Tarjan, R.E., A new approach to the maximum-flow problem, J. ACM, 35, 4, 921-940, (1988) · Zbl 0661.90031 [58] Gottlob, G.; Leone, N.; Scarcello, F., A comparison of structural CSP decomposition methods, (), 394-399 · Zbl 0952.68044 [59] Haken, A., The intractability of resolution, Theoret. comput. sci., 39, 297-308, (1985) · Zbl 0586.03010 [60] Huang, G., Constructing Craig interpolation formulas, (), 181-190 [61] Inoue, K., Linear resolution for consequence finding, Artificial intelligence, 56, 2-3, 301-353, (1992) · Zbl 0805.68105 [62] Klein, P.; Plotkin, S.A.; Rao, S., Excluded minors, network decomposition, and multicommodity flow, (), 682-690 · Zbl 1310.90017 [63] Kloks, T., Treewidth: computations and approximations, Lecture notes in computer science, vol. 842, (1994), Springer Berlin · Zbl 0825.68144 [64] Kohlas, J.; Haenni, R.; Moral, S., Propositional information systems, J. logic comput., 9, 5, 651-681, (1999) · Zbl 0941.03030 [65] Krajiček, J., Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. symbolic logic, 62, 2, 457-486, (1997) · Zbl 0891.03029 [66] Lauritzen, S.L.; Spiegelhalter, D.J., Local computations with probabilities on graphical structures and their application to expert systems, J. roy. statist. soc. B, 50, 2, 157-224, (1988) · Zbl 0684.68106 [67] R.C.-T. Lee, A completeness theorem and a computer program for finding theorems derivable from given axioms, PhD Thesis, University of California, Berkeley, 1967 [68] Leighton, T.; Rao, S., An approximate MAX-flow MIN-cut theorem for uniform multicommodity flow problems with applications to approximation algorithms, (), 422-431 [69] Lenat, D.B., Cyc: a large-scale investment in knowledge infrastructure, Comm. ACM, 38, 11, 33-38, (1995) [70] Lin, F., On strongest necessary and weakest sufficient conditions, (), 167-175 [71] Lloyd, J.W.; Topor, R.W., A basis for deductive database systems, J. logic programming, 2, 93-109, (1985) · Zbl 0583.68056 [72] Loveland, D.W., Automated theorem proving: A logical basis. fundamental studies in computer science, (1978), North-Holland Amsterdam [73] MacCartney, B.; McIlraith, Sh.; Amir, E.; Uribe, T., Practical partition-based theorem proving for large knowledge bases, (), 89-96 [74] Marquis, P., Knowledge compilation using theory prime implicates, (), 837-843 [75] Marquis, P., Consequence finding algorithms, () · Zbl 1015.68197 [76] McCarthy, J.; Buvač, S., Formalizing context (expanded notes), (), 13-50 · Zbl 0953.03517 [77] S. McIlraith, Logic-based abductive inference, Technical Report KSL-98-19, Knowledge Systems Lab, Department of Computer Science, Stanford University, 1998 [78] McIlraith, S.; Amir, E., Theorem proving with structured theories, (), 624-631 [79] A.R. Meyer, A note on the length of Craig’s interpolants Technical Memo MIT/LCS/TM-183, Massachusetts Institute of Technology, Laboratory for Computer Science, 1980 [80] Minicozzi, E.; Reiter, R., A note on linear resolution strategies in consequence-finding, Artificial intelligence, 3, 175-180, (1972) · Zbl 0252.68049 [81] Nelson, G.; Oppen, D.C., Simplification by cooperating decision procedures, ACM trans. programming lang. syst., 1, 2, 245-257, (1979) · Zbl 0452.68013 [82] Park, T.J.; Van Gelder, A., Partitioning methods for satisfiability testing on large formulas, (), 748-762 · Zbl 1412.68252 [83] Pearl, J., Probabilistic reasoning in intelligent systems: networks of plausible inference, (1988), Morgan Kaufmann San Mateo, CA [84] Plaisted, D.A., The search efficiency of theorem proving strategies, (), 57-71 [85] Ringeissen, C., Cooperation of decision procedures for the satisfiability problem, (), 121-140 · Zbl 0945.03011 [86] Rish, I.; Dechter, R., Resolution versus search: two strategies for SAT, J. automat. reason., 24, 1-2, 225-275, (2000) · Zbl 0967.68147 [87] Robertson, N.; Seymour, P.D., Graph minors. II: algorithmic aspects of treewidth, J. algorithms, 7, 309-322, (1986) · Zbl 0611.05017 [88] Robinson, J.A., A machine-oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41, (1965) · Zbl 0139.12303 [89] I. Schiermeyer, Pure literal look ahead: an O($$1, 497^n$$) 3-satisfiability algorithm (extended abstract), Technical Report, University of Köln, 1996. Workshop on the Satisfiability Problem, Siena, April 29-May 3 [90] Selman, B.; Kautz, H., Domain-independent extensions to GSAT: solving large structured satisfiability problems, () [91] Selman, B.; Kautz, H.A.; Cohen, B., Noise strategies for local search, (), 337-343 [92] Selman, B.; Levesque, H.J.; Mitchell, D., A new method for solving hard satisfiability problems, (), 440-446 [93] Selman, B.; Mitchell, D.; Levesque, H., Generating hard satisfiability problems, (), 17-29 [94] Shafer, G.; Shenoy, P., Probability propagation, Ann. math. artificial intelligence, 2, 327-352, (1990) · Zbl 0875.68676 [95] Shi, J.; Malik, J., Normalized cuts and image segmentation, (), 731-737 [96] Shoikhet, K.; Geiger, D., A practical algorithm for finding optimal triangulations, (), 185-190 [97] Shostak, R.E., Deciding combinations of theories, J. ACM, 31, 1-12, (1984) · Zbl 0629.68089 [98] Slagle, J.R., Interpolation theorems for resolution in lower predicate calculus, J. ACM, 17, 3, 535-542, (1970) · Zbl 0198.03601 [99] Slagle, J.R.; Chang, C.-L.; Lee, R.C.T., Completeness theorems for semantic resolution in consequence-finding, (), 281-285 [100] Slaney, J.; Surendonk, T.J., Combining finite model generation with theorem proving: problems and prospects, (), 141-156 · Zbl 0895.03004 [101] Stickel, M.E., A prolog technology theorem prover: a new exposition and implementation in prolog, Theoret. comput. sci., 104, 109-128, (1992) · Zbl 0771.68096 [102] Sutcliffe, G.C.J., A heterogeneous parallel deduction system, () [103] Suttner, C.B., Sptheo, J. automat. reason., 18, 253-258, (1997) [104] Tinelli, C.; Harandi, M.T., A new correctness proof of the Nelson-oppen combination procedure, (), 103-120 · Zbl 0893.03001 [105] Tseitin, G.S., On the complexity of proofs in propositional logics, Seminars in mathematics, 8, (1970) [106] Ullman, J.D., Principles of database and knowledge-base systems, vol. 1, (1988), Computer Science Press [107] Urquhart, A., Hard examples for resolution, J. ACM, 34, 1, 209-219, (1987) · Zbl 0639.68093
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.