Abstract
PTTP+GLiDeS is a semantically guided linear deduction theorem prover, built from PTTP [9] and MACE [7]. It takes problems in clause normal form (CNF), generates semantic information about the clauses, and then uses the semantic information to guide its search for a proof.
In the last decade there has been some work done in the area of semantic guidance, in a variety of first order theorem proving paradigms: SCOTT [8] is based on OTTER and is a forward chaining resolution system; CLIN-S [3] uses hyperlinking; RAMCS [2] uses constrained clauses to allow it to search for proofs and models simultaneously; and SGLD [11] is a chain format linear deduction system based on Graph Construction. Of these, CLIN-S and SGLD need to be supplied with semantics by the user. SCOTT uses FINDER [8] to generate models, and RAMCS generates its own models.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Brown, M., Sutcliffe, G.: PTTP+GLiDeS: Guiding Linear Deductions with Semantics. In: Foo, N.Y. (ed.) AI 1999. LNCS (LNAI), vol. 1747, pp. 244–254. Springer, Heidelberg (1999)
Caferra, R., Peltier, N.: Extending Semantic Resolution via Automated Model Building: Applications. In: Mellish, C.S. (ed.) Proceedings of the 14th International Joint Conference on Artificial Intelligence, pp. 328–334. Morgan Kaufmann, San Francisco (1995)
Chu, H., Plaisted, D.: Semantically Guided First-order Theorem Proving using Hyper-linking. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 192–206. Springer, Heidelberg (1994)
de Waal, D.A., Gallagher, J.P.: The Applicability of Logic Programming Analysis and Transformation to Theorem Proving. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 207–221. Springer, Heidelberg (1994)
Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning 8(2), 183–212 (1992)
Loveland, D.W.: A Simplified Format for the Model Elimination Theorem-Proving Procedure. Journal of the ACM 16(3), 349–363 (1969)
McCune, W.W.: A Davis-Putnam Program and its Application to Finite First- Order Model Search: Quasigroup Existence Problems. Technical Report Technical Report ANL/MCS-TM-194, Argonne National Laboratory, Argonne, USA (1994)
Slaney, J.K.: SCOTT: A Model-Guided Theorem Prover. In: Bajcsy, R. (ed.) Proceedings of the 13th International Conference on Artificial Intelligence, pp. 109–114. Morgan-Kaufman, San Francisco (1993)
Stickel, M.E.: A Prolog Technology Theorem Prover: A New Exposition and Im- plementation in Prolog. Technical Report Technical Note 464, SRI International, Menlo Park, USA (1989)
Sutcliffe, G.: Linear-Input Subset Analysis. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 268–280. Springer, Heidelberg (1992)
Sutcliffe, G.: The Semantically Guided Linear Deduction System. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 677–680. Springer, Heidelberg (1992)
Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brown, M., Sutcliffe, G. (2000). System Description: PTTP+GLiDeS Semantically Guided PTTP. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_32
Download citation
DOI: https://doi.org/10.1007/10721959_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive