Abstract
We examine different possibilities of coupling saturationbased theorem provers by exchanging positive/negative information. Positive information is given by facts that should be employed for proving a proof goal, negative information is represented by facts that do not appear to be useful. We introduce a basic model for cooperative theorem proving employing both kinds of information. We present theoretical results regarding the exchange of positive/negative information as well as practical methods that allow for a gain of efficiency in comparison with sequential provers. Finally, we report on experimental studies conducted in the areas unfailing completion and superposition.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Avenhaus and J. Denzinger. Distributing equational theorem proving. In Proc. 5th RTA, pages 62–76, Montreal, 1993. LNCS 690.
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.
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.
L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217–247, 1994.
J. Denzinger and M. Fuchs. Goal oriented equational theorem proving. In Proc. 18th KI-94, pages 343–354, Saarbrücken, 1994. LNAI 861.
J. Denzinger and D. Fuchs. Referees for teamwork. In Proc. FLAIRS '96, pages 454–458, Key West, 1996.
D. Fuchs and J. Denzinger. Cooperation in theorem proving by loosely coupled heuristics. Technical Report SR-97-03 (ftp://ftp.uni-kl.de/reports_unikl/computer_science/SEKI/1997/Fuchs.SR-97-03.ps.gz), University of Kaiserslautern, Kaiserslautern, 1997.
D. Fuchs. Coupling saturation-based provers by exchanging positive/negative information. Technical Report SR-97-07 (ftp://ftp.unikl.de/reports_uni-kl/computer_science/SEKI/1997/Fuchs.SR-97-07.ps.gz), University of Kaiserslautern, Kaiserslautern, 1997.
D. Fuchs. Inference Rights for Controlling Search in Generating Theorem Provers. In Proc. EPIA '97, pages 25–36, Coimbra, 1997. LNAI 1323.
W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory, Argonne, 1994.
G. Sutcliffe, C.B. Suttner, and T. Yemenis. The TPTP Problem Library. In CADE-12, pages 252–266, Nancy, 1994. LNAI 814.
G. Sutcliffe. A heterogeneous parallel deduction system. In Proc. FGCS'92 Workshop W3, 1992.
C. Weidenbach, B. Gaede, and G. Rock. Spass & Flotter Version 0.42. In Proc. CADE-13, pages 141–145, New Brunswick, 1996. LNAI 1104.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Fuchs, D. (1998). Coupling saturation-based provers by exchanging positive/negative information. In: Nipkow, T. (eds) Rewriting Techniques and Applications. RTA 1998. Lecture Notes in Computer Science, vol 1379. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0052379
Download citation
DOI: https://doi.org/10.1007/BFb0052379
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64301-2
Online ISBN: 978-3-540-69721-3
eBook Packages: Springer Book Archive