[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

DCTP - A Disconnection Calculus Theorem Prover - System Abstract

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2001)

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

Included in the following conference series:

Abstract

We describe the theorem prover DCTP, which is an implementation of the disconnection tableau calculus, a confluent tableau method, in which free variables are treated in a non-rigid manner. In contrast to most other free-variable tableau variants, the system can also be used for model generation. We sketch the underlying calculus and its refinements, and present the results of an experimental evaluation.

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.

Similar content being viewed by others

References

  1. P. Baumgartner, N. Eisinger, and U. Furbach. A confluent connection calculus. In Proceedings, CADE-16, Trento, LNAI 1632, pp. 329–343. Springer, 1999.

    Google Scholar 

  2. P. Baumgartner, U. Furbach, and I. Niemelä. Hyper tableaux. In Proceedings, JELIA-96, LNAI 1126, pp. 1–17, Springer, 1996.

    Google Scholar 

  3. Jean-Paul Billon. The disconnection method: a confluent integration of unification in the analytic framework. In Proceedings of the 5th TABLEAUX, Terrasini, LNAI 1071, pp. 110–126, Springer, 1996.

    Google Scholar 

  4. S.-J. Lee and D. Plaisted. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, pp. 25–42, 1992.

    Google Scholar 

  5. Reinhold Letz, Klaus Mayr, and C. Goller. Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning, 13(3):297–338, December 1994.

    Article  MathSciNet  MATH  Google Scholar 

  6. Reinhold Letz, Johann Schumann, Stephan Bayerl, and Wolfgang Bibel. SETHEO: A high-performance theorem prover. Journal of Automated Reasoning, 8(2):183–212, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  7. Stephan Schulz. System Abstract: E 0.61. In Proc. of the 1st IJCAR, Siena, LNAI. Springer, 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische Universität München, D-80290, Munich, Germany

    Reinhold Letz & Gernot Stenz

Authors
  1. Reinhold Letz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gernot Stenz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Automated Reasoning Project and Department of Computer Science, Australian National University, Canberra, ACT, 0200, Australia

    Rajeev Goré

  2. AG Theoretische Informatik und Logik, Institut für Computersprachen, Technische Universität Wien, Favoritenstr. 9, E185-2, 1040, Wien, Austria

    Alexander Leitsch

  3. Institut für Informatik, Technische Universität München, 80290, München, Germany

    Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Letz, R., Stenz, G. (2001). DCTP - A Disconnection Calculus Theorem Prover - System Abstract. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_30

Download citation

  • DOI: https://doi.org/10.1007/3-540-45744-5_30

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42254-9

  • Online ISBN: 978-3-540-45744-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation