Dissolver: A dissolution-based theorem prover | SpringerLink
Skip to main content
Springer Nature Link
Log in

Dissolver: A dissolution-based theorem prover

  • Conference paper
  • First Online:
10th International Conference on Automated Deduction (CADE 1990)

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

Included in the following conference series:

  • 172 Accesses

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

References

  1. Chang, C.L., and Lee, R.C.T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.

    Google Scholar 

  2. Lawrence, J., and Starkey, J. Experimental tests of resolution-based theorem proving strategies. CS-74-011, Computer Sci. Dept., Washington State Univ., April 1974.

    Google Scholar 

  3. McCune, W. Otter 1.0 user's guide. Technical Report ANL-88/44, Argonne National Laboratory, Argonne, IL.

    Google Scholar 

  4. Murray, N.V. An experimental theorem prover using fast unification and vertical path graphs. Proceedings of the Fourth National Conference on Canadian Society of Computational Studies of Intelligence, Saskatoon, Canada, May 1982, 125–131.

    Google Scholar 

  5. Murray, N.V., and Rosenthal, E. Path dissolution: A strongly complete rule of inference. Proceedings of the 6 th National Conference on Artificial Intelligence, Seattle, WA, July 12–17, 1987, 161–166.

    Google Scholar 

  6. Murray, N.V., and Rosenthal, E. Inferencing on an arbitrary set of links. Proceedings of the 2nd International Symposium on Methodologies for Intelligent Systems, Charlotte, NC, October 1987. In Methodologies for Intelligent Systems, (Ras, Z., and Zemankova, M., eds.) North-Holland, 1987, 416–423.

    Google Scholar 

  7. Murray, N.V., and Rosenthal, E. An implementation of a dissolution-based system employing theory links. Proceedings of the 9th International Conference on Automated Deduction, Argonne Nat. Lab., May 23–26, 1988. In Lecture Notes in Computer Science, Springer-Verlag, Vol. 310, 658–674.

    Google Scholar 

  8. Newborn, M. The Great Theorem Prover. Newborn Software, Westmount, Quebec, 1989.

    Google Scholar 

  9. Zhang, H., and Kapur, D. First order theorem proving using conditional rewrite rules. Proceedings of CADE-9, Lecture Notes in Computer Science, vol. 310, 1–20, Springer-Verlag, Argonne National Laboratories, Argonne, IL, May 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, SUNY Albany, 12222, Albany, NY

    Neil V. Murray

  2. Dept. of Mathematics, U. of New Haven, 06516, West Haven, CT

    Erik Rosenthal

Authors
  1. Neil V. Murray
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Erik Rosenthal
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mark E. Stickel

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Murray, N.V., Rosenthal, E. (1990). Dissolver: A dissolution-based theorem prover. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_132

Download citation

  • DOI: https://doi.org/10.1007/3-540-52885-7_132

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52885-2

  • Online ISBN: 978-3-540-47171-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation