Skip to main content
SpringerLink
Log in

Nested resolution

  • Special Deduction Systems
  • Conference paper
  • First Online:
8th International Conference on Automated Deduction (CADE 1986)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 230))

Included in the following conference series:

Abstract

In this paper we introduce nested resolution, a new nonclausal resolution rule which offers shorter proofs than are possible using conventional nonclausal resolution. Nested resolution also has a local flavor that makes it particularly suitable for parallel implementation. Completeness and soundness proofs are given.

This research was supported in part by the National Science Foundation under grants DCR-8512356 and MCS-82-14523, by DARPA under Contract N00039-84-C-0211, by the United States Air Force Office of Scientific Research under Contract AFOSR-81-0014, by the Office of Naval Research under Contract N00014-84-C-0706, by the United States Army under contract DAJA-45-84-C-0040, and by a contract from the International Business Machines Corporation.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Manna and Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, Vol. 2, No 1, 1980.

    Google Scholar 

  2. Manna and Waldinger, Special relations in automated deduction. Journal of the ACM., Vol 33, No 1, Jan 1986.

    Google Scholar 

  3. Malachi, Nonclausal logic programming. Ph.D. Thesis. Stanford University. March 1986.

    Google Scholar 

  4. Murray, Completely non-clausal theorem proving. Artificial Intelligence, Vol 18, 1982.

    Google Scholar 

  5. Robinson, A machine-oriented logic based on the resolution principle. Journal of the ACM., Vol. 12, No 1, Jan 1965

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Stanford University, USA

    Jonathan Traugott

Authors
  1. Jonathan Traugott
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jörg H. Siekmann

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Traugott, J. (1986). Nested resolution. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_106

Download citation

  • DOI: https://doi.org/10.1007/3-540-16780-3_106

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16780-8

  • Online ISBN: 978-3-540-39861-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation