Skip to main content
SpringerLink
Log in

Improving the Efficiency of Reasoning Through Structure-Based Reformulation

  • Conference paper
  • First Online:
Abstraction, Reformulation, and Approximation (SARA 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1864))

Abstract

We investigate the possibility of improving the efficiency of reasoning through structure-based partitioning of logical theories, combined with partitionbased logical reasoning strategies. To this end, we provide algorithms for reasoning with partitions of axioms in first-order and propositional logic. We analyze the computational benefit of our algorithms and detect those parameters of a partitioning that influence the efficiency of computation. These parameters are the number of symbols shared by a pair of partitions, the size of each partition, and the topology of the partitioning. Finally, we provide a greedy algorithm that automatically reformulates a given theory into partitions, exploiting the parameters that influence the efficiency of computation.

Much of the material presented in this abstract appeared in [2].

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Amir. (De)composition of situation calculus theories. In Proc. National Conference on Artificial Intelligence (AAAI’ 00) AAAI Press/MIT Press, 2000. To appear.

    Google Scholar 

  2. E. Amir and S. McIlraith. Partition-based logical reasoning. In Intl. Conf. on Knowledge Representation and Reasoning (KR’ 2000), pages 389–400, 2000.

    Google Scholar 

  3. F. Baader and K. U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In 11th Intl. conf. on automated deduction, volume 607 of LNAI, pages 50–65. Springer-Verlag, 1992.

    Google Scholar 

  4. A. Becker and D. Geiger. A sufficiently fast algorithm for finding close to optimal junction trees. In Proc. Twelfth Conference on Uncertainty in Artificial Intelligence (UAI’ 96), pages 81–89. Morgan Kaufmann, 1996.

    Google Scholar 

  5. M. P Bonacina. Experiments with subdivision of search in distributed theorem proving. In Markus Hitz and Erich Kaltofen, editors, Proceedings of the Second International Symposium on Parallel Symbolic Computation (PASCO97), pages 88–100. ACM Press, 1997.

    Google Scholar 

  6. M. P. Bonacina. A taxonomy of theorem-proving strategies. In Artificial Intelligence Today-Recent Trends and Developments, volume 1600 of LNAI, pages 43–84. Springer, 1999.

    Google Scholar 

  7. M. P Bonacina and J. Hsiang. Parallelization of deduction strategies: an analytical study. Journal of Automated Reasoning, 13:1–33, 1994.

    Article  MathSciNet  Google Scholar 

  8. M. P Bonacina and J. Hsiang. Distributed deduction by Clause-Diffusion: distributed contraction and the Aquarius prover. J. of Symbolic Computation, 19:245–267, March 1995.

    Google Scholar 

  9. P.E. Bonzon. A reflective proof system for reasoning in contexts. In Proc. Nat’ l Conf. on Artificial Intelligence (AAAI’ 97), pages 398–403, 1997.

    Google Scholar 

  10. R. Boppana and M. Sipser. The complexity of finite functions. In Handbook of Theoretical Computer Science, volume 1. Elsevier and MIT Press, 1990.

    Google Scholar 

  11. C. Boutilier, R. Dearden, and M. Goldszmidt. Exploiting structure in policy construction. In14thIntl. Joint Conf. on Artificial Intelligence (IJCAI’ 95), pages 1104–1111, 1995.

    Google Scholar 

  12. A. Carbone. Interpolants, cut elimination and flow graphs for the propositional calculus. Annals of Pure and Applied Logic, 83(3):249–299, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  13. P. Cohen, R. Schrag, E. Jones, A. Pease, A. Lin, B. Starr, D. Gunning, and M. Burke. The DARPA high-performance knowledge bases project. AI Magazine, 19(4):25–49, 1998.

    Google Scholar 

  14. S. A. Cook and D. G. Mitchell. Finding hard instances of the satisfiability problem: a survey. In Dimacs Series in Discrete Math. and Theoretical Comp. Sci, volume 35. AMS, 1997.

    Google Scholar 

  15. R. Cowen and K. Wyatt. BREAKUP: A preprocessing algorithm for satisfiability testing of CNF formulas. Notre Dame J. of Formal Logic, 34(4):602–606, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  16. W. Craig. Linear reasoning. a new form of the herbrand-gentzen theorem. J. of Symbolic Logic, 22:250–268, 1957.

    Article  MATH  MathSciNet  Google Scholar 

  17. A. Darwiche. Model-based diagnosis using structured system descriptions. Journal of Artificial Intelligence Research, 8:165–222, 1998.

    MATH  MathSciNet  Google Scholar 

  18. R. Dechter. Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition. Artificial Intelligence, 41(3):273–312, 1990.

    Article  Google Scholar 

  19. R. Dechter and J. Pearl. Tree clustering for constraint networks. Artificial Intelligence, 38:353–366, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  20. R. Dechter and I. Rish. Directional resolution: The davis-putnam procedure, revisited. In Intl. Conf. on Knowledge Representation and Reasoning (KR’ 94), pages 134–145. Morgan Kaufmann, 1994.

    Google Scholar 

  21. R. Fikes and A. Farquhar. Large-scale repositories of highly expressive reusable knowledge. IEEE Intelligent Systems, 14(2), 1999.

    Google Scholar 

  22. G. Gallo and G. Urbani. Algorithms for testing the satisfiability of propositional formulae. J. of Logic Programming, 7:45–61, 1989.

    Article  MathSciNet  MATH  Google Scholar 

  23. F Giunchiglia. Getfol manual-getfol version 2.0. Technical Report DIST-TR-92-0010, DIST-University of Genoa, 1994. http://ftp.mrg.dist.unige.it/pub/mrg-ftp/92-0010.ps.gz.

  24. A. Haken. The intractability of resolution. theoretical computer science, 39:297–308, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  25. K. Inoue. Linear resolution for consequence finding. Artificial Intelligence, 56(2–3):301–353, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  26. J. Krajiček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. of Symbolic Logic, 62(2):457–486, 1997.

    Article  MATH  Google Scholar 

  27. R. C. Lee. A Completeness Theorem and a Computer Program for Finding Theorems Derivable from Given Axioms PhD thesis, University of California, Berkeley, 1967.

    Google Scholar 

  28. D. B. Lenat. Cyc: A large-scale investment in knowledge infrastructure. Communications of the ACM, 38(11):13–38, 1995.

    Google Scholar 

  29. P. Marquis. Knowledge compilation using theory prime implicates. In 14th Intl. Joint Conf. on Artificial Intelligence (IJCAI’ 95), pages 837–843, 1995.

    Google Scholar 

  30. J. McCarthy and S. Buvac. Formalizing Context (Expanded Notes). In A. Aliseda, R.J. van Glabbeek, and D. Westerståhl, editors, Computing Natural Language, volume 81 of CSLI Lecture Notes, pages 13–50. Center for the Study of Language and Information, Stanford U., 1998.

    Google Scholar 

  31. E. Minicozzi and R. Reiter. A note on linear resolution strategies in consequence-finding. Artificial Intelligence, 3:175–180, 1972.

    Article  MATH  MathSciNet  Google Scholar 

  32. G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Trans. on Programming Languages and Systems, 1(2):245–257, 1979.

    Article  MATH  Google Scholar 

  33. T. J. Park and A. VanGelder. Partitioning methods for satisfiability testing on large formulas. In Proc. Intl. Conf. on Automated Deduction (CADE-13), pages 748–762. Springer-Verlag, 1996.

    Google Scholar 

  34. J. Pearl. Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference Morgan Kaufmann, 1988.

    Google Scholar 

  35. D. A. Plaisted. The search efficiency of theorem proving strategies. In Proc. Intl. Conf. on Automated Deduction (CADE-12), pages 57–71, 1994.

    Google Scholar 

  36. C. Ringeissen. Cooperation of decision procedures for the satisfiability problem. In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany), Applied Logic, pages 121–140. Kluwer, March 1996.

    Google Scholar 

  37. I. Rish and R. Dechter. Resolution versus search: two strategies for SAT. J. of Approximate Reasoning, To appear, 2000.

    Google Scholar 

  38. I. Schiermeyer. Pure literal look ahead: an O(1, 497n) 3-satisfiability algorithm (extended abstract). Technical report, University of Köln, 1996. Workshop on the Satisfiability Problem, Siena April 29-May 3.

    Google Scholar 

  39. B. Selman and H. Kautz. Domain-independent extensions to GSAT: Solving large struc tured satisfiability problems. In 13th Intl. Joint Conf. on Artificial Intelligence (IJCAI’ 93), 1993.

    Google Scholar 

  40. R. E. Shostak. Deciding combinations of theories. J. of the ACM, 31:1–12, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  41. J. R. Slagle. Interpolation theorems for resolution in lower predicate calculus. J. of the ACM, 17(3):535–542, July 1970.

    Google Scholar 

  42. J. R. Slagle, C.-L. Chang, and R. C. T. Lee. Completeness theorems for semantic resolution in consequence-finding. In 1st Intl. Joint Conf. on Artificial Intelligence (IJCAI’ 69), pages 281–285, 1969.

    Google Scholar 

  43. C. B. Suttner. SPTHEO. Journal of Automated Reasoning, 18:253–258, 1997.

    Article  Google Scholar 

  44. C. Tinelli and M. T. Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In F. Baader and K.U. Schulz, editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany), Applied Logic, pages 103–120. Kluwer, March 1996.

    Google Scholar 

  45. J. D. Ullman. Principles of Database and knowledge-base systems, volume 1. Computer Science Press, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Stanford University, Stanford, CA, 94305

    Eyal Amir

  2. Knowledge Systems Lab Department of Computer Science, Stanford University, Stanford, CA, 94305

    Sheila McIlraith

Authors
  1. Eyal Amir
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sheila McIlraith
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, University of Nebraska - Lincoln, 115 Ferguson Hall, Lincoln, NE, 68588-0115

    Berthe Y. Choueiry

  2. Department of Computer Science, University of York, Heslington, York, Y010 5DD, UK

    Toby Walsh

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Amir, E., McIlraith, S. (2000). Improving the Efficiency of Reasoning Through Structure-Based Reformulation. In: Choueiry, B.Y., Walsh, T. (eds) Abstraction, Reformulation, and Approximation. SARA 2000. Lecture Notes in Computer Science(), vol 1864. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44914-0_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-44914-0_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67839-7

  • Online ISBN: 978-3-540-44914-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation