The addition of bounded quantification and partial functions to a computational logic and its theorem prover
Tóm tắt
We describe an extension to our quantifier-free computational logic to provide the expressive power and convenience of bounded quantifiers and partial functions. By quantifier we mean a formal construct which introduces a bound or indicial variable whose scope is some subexpression of the quantifier expression. A familiar quantifier is the Σ operator which sums the values of an expression over some range of values on the bound variable. Our method is to represent expressions of the logic as objects in the logic, to define an interpreter for such expressions as a function in the logic, and then define quantifiers as ‘mapping functions’. The novelty of our approach lies in the formalization of the interpreter and its interaction with the underlying logic. Our method has several advantages over other formal systems that provide quantifiers and partial functions in a logical setting. The most important advantage is that proofs not involving quantification or partial recursive functions are not complicated by such notions as ‘capturing’, ‘bottom’, or ‘continuity’. Naturally enough, our formalization of the partial functions is nonconstructive. The theorem prover for the logic has been modified to support these new features. We describe the modifications. The system has proved many theorems that could not previously be stated in our logic. Among them are:
Tài liệu tham khảo
Boyer, R.S. and Moore, J S., A Computational Logic. Academic Press, New York (1979).
Boyer, R. S. and Moore, J S., ‘Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures’, In The Correctness Problem in Computer Science, (R. S. Boyer and J. S. Moore, Eds.) Academic Press, London (1981).
Boyer, R. S., and Moore, J S., ‘A Verification Condition Generator for FORTRAN’. In The Correctness Problem in Computer Science (R. S. Boyer and J S. Moore, Eds) Academic Press, London (1981).
Boyer, R. S., and Moore, J S., ‘The Mechancial Verification of a FORTRAN Square Root Program’. SRI International (1981).
Boyer, R. S., and Moore, J S., ‘MJRTY — A Fast Majority Vote Algorithm’. Technical Report ICSCA-CMP-32, Institute for Computing Science and Computer Applications, University of Texas at Austin (1982).
Boyer, R. S., and Moore, J S., ‘Proof Checking the RSA Public Key Encryption Algorithm’. American Mathematical Monthly 91 181–189, (1984).
Boyer, R. S., and Moore, J S., ‘A Mechanical Proof of the Unsolvability of the Halting Problem’. JACM 31 441–458 (1984).
Boyer, R. S. and Moore, R S., ‘Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study with Linear Arithmetic’, In Machine Intelligence 11, Oxford University Press (to appear, 1988).
Boyer R. S. and Moore J S., ‘The User's Manual for A Computational Logic’, Technical Report 18, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, TX 78703.
Boyer, R. S. and Moore, J S., ‘A Mechanical Proof of the Turing Completeness of Pure Lisp’. In Automated Theorem Proving: After 25 Years (W. W. Bledsoe and D. W. Loveland, Eds.) American Mathematical Society, Providence, R.I., pp. 133–167 (1984).
Boyer, R. S., Green, M. W., and Moore, J S., ‘The Use of a Formal Simulator to Verify a Simple Real Time Control Program’. Technical Report ICSCA-CMP-29, University of Texas at Austin (1982).
Church, A. Introduction to Mathematical Logic. Princeton University Press, Princeton, New Jersey, 1956.
Di Vito, Benedetto Lorenzo, ‘Verification of Communications Protocolsand Abstract Process Models’. PhD Thesis ICSCA-CMP-25, Institute for Computing Science and Computer Applications, University of Texas at Austin (1982).
Gordon, M. J. C., The Denotational Description of Programming Languages. Springer-Verlag, New York (1979).
Huang, C.-H., and Lengauer, C. ‘The Automated Proof of a Trace Transformation for a Bitonic Sort’. Tech. Rept. TR-84-30, Department of Computer Sciences, The University of Texas at Austin, Oct. (1984).
Hunt, Warren A. Jr. ‘FM8501: A Verified Microprocessor’. PhD Thesis, University of Texas at Austin (1985).
Kelley, J.. General Topology. D. van Nostrand, Princeton, New Jersey, 1955.
Lengauer, C., ‘On the Role of Automated Theorem Proving in the Compile-Time Derivation of Concurrency’. Journal of Automated Reasoning 1, 75–101 (1985).
Lengauer, C., and Huang, C.-H., ‘A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks, and Its Proof’. Tech. Rept. TR-85-23, Department of Computer Sciences, The University of Texas at Austin, Oct. (1985).
Manna, Z., Mathematical Theory of Computation. McGraw-Hill Book Company, New York, New York (1974).
McCarthy, J. et al., LISP 1.5 Programmer's Manual. The MIT Press, Cambridge, Massachusetts, 1965.
Morse, A. P., A Theory of Sets. Academic Press, New York, 1965.
Russinoff, David M., ‘A Mechanical Proof of Wilson's Theorem’. Department of Computer Sciences, University of Texas at Austin (1983).
Shankar, N., ‘Towards Mechanical Metamathematics’. Journal of Automated Reasoning 1, 407–434 (1985)
Shankar, N., ‘A Mechanical Proof of the Church-Rosser Theorem’ in ‘Proof Checking Metamathematics’, PhD Thesis, University of Texas at Austin (1986).
Shankar, N. ‘Checking the proof of Gödel's incompleteness theorem’ in ‘Proof Checking Metamathematics’, PhD Thesis, University of Texas at Austin (1986).
Stoy, J. E., Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, Cambridge, Massachusetts (1977).
Teitelman, W., INTERLISP Reference Manual. Xerox Palo Alto Research Center, 3333 Coyote Hill Road, Palo Alto, Ca., (1978).
Turner, D. A. ‘A New Implementation Technique for Applicative Languages’. Software—Practice and Experience 9 31–49 (1979).