Skip to main content
SpringerLink
Log in

Requirement-Based Cooperative Theorem Proving

  • Conference paper
  • First Online:
Logics in Artificial Intelligence (JELIA 1998)

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

Included in the following conference series:

Abstract

We examine an approach for demand-driven cooperative theorem proving that is well-suited for saturation-based theorem provers. We briefly point out some problems arising from the use of common success-driven cooperation methods, and we propose the application of our approach of requirement-based cooperative theorem proving. This approach aims to allowing more orientation on current needs of provers in comparison with conventional cooperation concepts. We introduce an abstract framework for requirement-based cooperation and describe two instantiations of it: Requirement-based exchange of facts and sub-problem division and transfer via requests. Finally, we report on an experimental study conducted in the areas of superposition and unfailing completion.

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. J. Avenhaus, J. Denzinger, and M. Fuchs. DISCOUNT: A System For Distributed Equational Deduction. In Proc. 6th RTA, pages 397–402, Kaiserslautern, 1995. LNCS 914.

    Google Scholar 

  2. L. Bachmair, N. Dershowitz, and D.A. Plaisted. Completion without Failure. In Coll. on the Resolution of Equations in Algebraic Structures. Academic Press, Austin, 1989.

    Google Scholar 

  3. L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  4. M.P. Bonacina and J. Hsiang. The Clause-Diffusion methodology for distributed deduction. Fundamenta Informaticae, 24:177–207, 1995.

    MATH  MathSciNet  Google Scholar 

  5. M.P. Bonacina. On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method. Journal of Symbolic Computation, 21(4):507–522, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. J. Denzinger. Knowledge-based distributed search using teamwork. In Proc. ICMAS-95, pages 81–88, San Francisco, 1995. AAAI-Press.

    Google Scholar 

  7. J. Denzinger and D. Fuchs. Enhancing conventional search systems with multi-agent techniques: a case study. In Proc. ICMAS-98, Paris, France, 1998.

    Google Scholar 

  8. W. Ertel. OR-Parallel Theorem Proving with Random Competition. In Proceedings of LPAR’92, pages 226–237, St. Petersburg, Russia, 1992. Springer LNAI 624.

    Google Scholar 

  9. D. Fuchs and J. Denzinger. Knowledge-based cooperation between theorem provers by TECHS. Technical Report SR-97-11, University of Kaiserslautern, Kaiserslautern, 1997.

    Google Scholar 

  10. D. Fuchs. Coupling saturation-based provers by exchanging positive/negative information. In Proc. 9th RTA, pages 317–331, Tsukuba, Japan, 1998. LNCS 1379.

    Google Scholar 

  11. D. Fuchs. Requirement-based cooperative theorem proving. Technical Report SR-98-02 (ftp://ftp.uni-kl.de/reports_uni-kl/computer_science/SEKI/1998/Fuchs.SR-98-02.ps.gz), University of Kaiserslautern, Kaiserslautern, 1998.

    Google Scholar 

  12. J. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. ICALP87, pages 54–71. LNCS 267, 1987.

    Google Scholar 

  13. G. Sutcliffe and C.B. Suttner. The results of the cade-13 ATP system competition. Journal of Automated Reasoning, 18(2):271–286, 1997.

    Article  MathSciNet  Google Scholar 

  14. G. Sutcliffe, C.B. Suttner, and T. Yemenis. The TPTP Problem Library. In CADE-12, pages 252–266, Nancy, 1994. LNAI 814.

    Google Scholar 

  15. G. Sutcliffe. A heterogeneous parallel deduction system. In Proc. FGCS’92 Workshop W3, 1992.

    Google Scholar 

  16. C. Weidenbach, B. Gaede, and G. Rock. Spass & Flotter Version 0.42. In Proc. CADE-13, pages 141–145, New Brunswick, 1996. LNAI 1104.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Kaiserslautern, Germany

    Dirk Fuchs

Authors
  1. Dirk Fuchs
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Maryland, College Park, Maryland, 20742, USA

    Jürgen Dix

  2. I.R.I.T. Université Paul Sabatier, 118 route de Narbonne, F-31062, Toulouse Cedex, France

    Luís Fariñas del Cerro

  3. Fachbereich 4: Informatik, Universität Koblenz, Rheinau 1, D-56075, Koblenz, Germany

    Ulrich Furbach

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fuchs, D. (1998). Requirement-Based Cooperative Theorem Proving. In: Dix, J., del Cerro, L.F., Furbach, U. (eds) Logics in Artificial Intelligence. JELIA 1998. Lecture Notes in Computer Science(), vol 1489. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49545-2_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-49545-2_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65141-3

  • Online ISBN: 978-3-540-49545-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation