Abstract
Logicians have long realized that the language of first order logic has great expressive power. In the early days of computers they tried to program the art of theorem-proving in the hope that the machine would then provide a steady stream of new and interesting results. Even although these hopes have faded more and more people are writing theorem proving programs. Why? Because the computer can extract information from the proofs of even simple theorems, that it can use for some other purpose. The techniques for doing this have been developed for theorem-provers that use local methods like resolution. Here we shall describe a technique for extraction of information from global theorem-provers of the kind developed by Prawitz, Kanger and others.
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.
Bibliography
R. S. Boyer and J. S. Moore, ‘The Sharing of Structure in Theorem Proving Programs’, Machine Intelligence, Edinburgh Univ. Press, 7 (1972), pp. 101–116.
C. L. Chang and R. C. T. Lee, ‘Symbolic Logic and Mechanical Theorem Proving’, Academic Press, 1973.
J. L. Darlington, ‘Deductive Plan Formulation in Higher Order Logic’, Machine Intelligence, Edinburgh Univ. Press 7 (1972), pp. 129–137.
R. E. Fikes, ‘REF-ARF, A System for Solving Problems Stated as Procedures’, Artificial Intelligence, North-Holland Publ. Co. Amsterdam 1, pp. 27–120.
R. E. Fikes and N. J. Nilsson, ‘STRIPS, A New Approach to the Application of Theorem Proving to Problem Solving’, Artificial Intelligence, North-Holland Publ. Co. Amsterdam 2 (1971), pp. 189–208.
R. W. Floyd, Toward Interactive Design of Correct Programs, Proc. IFIP Congress (1971) N. Holland Publ. Co., Amsterdam, pp. 1–4.
C. Cordell Green, ‘Theorem Proving by Resolution as a Basis for Question Answering Systems’, Machine Intelligence, Edinburgh Univ. Press 4 (1969), pp. 183–208.
P. J. Hayes, ‘Robotologic’, Machine Intelligence, Edinburgh Univ. Press 5 (1970), pp. 533–554.
P. J. Hayes, ‘A Logic of Actions’, Machine Intelligence, Edinburgh Univ. Press 6 (1971), pp. 495 - 520.
S. Kanger: A Simplified Proof Method for Elementary Logic, Computer Programming and Formal Systems (ed. by P. Braffort and D. Hirschberg ), N. Holland Publ. Co., Amsterdam, 1963.
T. A. Linden, A Summary of Programs Toward Proving Program Correctness, AFIPS Proc. Fall Joint Comp. Conf. (1972), N. Holland Publ. Co., Amsterdam, pp. 201–211.
D. Luckham and N. J. Nilsson, ‘Extracting Information from Resolution Proof Trees’, Artificial Intelligence, North-Holland Publ. Co. Amsterdam. 2 (1971), pp. 27–54.
Z. Manna, S. Ness, and J. Vuillemin, ‘Fixpoint Approach to Theory of Computation’, Comm. Ass. Comp. Mach. 15 (1972), 528–536.
Z. Manna and R. J. Waldinger, ‘Towards Automatic Program Synthesis’, Comm. Ass. Comp. Mach. 14 (1971), 151–165.
B. H. Mayoh, Sprog, logik og tcenkende maskiner, Sprog og Virkelighed (ed. by M. Jacobsen ), Gyldendal, 1973.
J. McCarthy and P. J. Hayes, ‘Some Philosophical Problems from the Standpoint of Artificial Intelligence’, Machine Intelligence, Edinburgh Univ. Press 4 (1969), pp. 463–502.
N. J. Nilsson, Problem Solving Methods in Artificial Intelligence, McGraw-Hill, 1971.
D. Prawitz, ‘Advances and Problems in Mechanical Proof Procedures’, Machine Intelligence, Edinburgh Univ. Press 4 (1969), pp. 59–72.
19]J. A. Robinson, ‘Computational Logic, the Unification Computation’, Machine Intelligence, Edinburgh Univ. Press 6 (1971), pp. 63–72.
E. Sandewall: ‘Representing Natural Language Information in Predicate Calculus’, Machine Intelligence, Edinburgh Univ. Press 6 (1971), 255–280.
E. Sandewall, ‘Formal Methods in the Design of Question-Answering Systems’, Artificial Intelligence, North-Holland Publ. Co. Amsterdam. 2 (1971), pp. 129–146.
R. F. Simmons, ‘Natural Language Question-Answering Systems’, Comm. Ass. Comp. Mach. 13 (1970), 15–30.
A. M. Turing, ‘Computing Machinery and Intelligence’, Mind 59 (1950). reprinted in Mind and Machine (ed. by A. R. Anderson ), Prentice Hall, 1964.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1974 D. Reidel Publishing Company, Dordrecht-Holland
About this chapter
Cite this chapter
Mayoh, B.H. (1974). Extracting Information from Logical Proofs. In: Stenlund, S., Henschen-Dahlquist, AM., Lindahl, L., Nordenfelt, L., Odelstad, J. (eds) Logical Theory and Semantic Analysis. Synthese Library, vol 63. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-2191-3_6
Download citation
DOI: https://doi.org/10.1007/978-94-010-2191-3_6
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-2193-7
Online ISBN: 978-94-010-2191-3
eBook Packages: Springer Book Archive