Advertisement

Classical propositional decidability via Nuprl proof extraction

  • James L. Caldwell
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

Abstract

This paper highlights a methodology of Nuprl proof that results in efficient programs that are more readable than those produced by other established methods for extracting programs from proofs. We describe a formal constructive proof of the decidability of a sequent calculus for classical propositional logic. The proof is implemented in the Nuprl system and the resulting proof object yields a “correct-by-construction≓ program for deciding propositional sequents. If the sequent is valid, the program reports that fact; otherwise, the program returns a counter-example in the form of a falsifying assignment. We employ Kleene's strong three-valued logic to give more informative counter-examples, it is also shown how this semantics agrees with the standard two-valued presentation.

Keywords

Disjoint Union Type Theory Sequent Calculus Derivation Tree Partial Assignment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Stuart F. Allen. From dy/dx to []P: A matter of notation. In Proceedings of User Interfaces for Theorem Provers 1998. Eindhoven University of Technology, July 1998.Google Scholar
  2. 2.
    R. S. Boyer and J. S. Moore. A Computational Logic. NY:Academic Press, 1979.Google Scholar
  3. 3.
    James Caldwell. Extracting propositional decidability: A proof of prepositional decidability in constructive type theory and its extract. Available at http://simon.cs.cornell.edu/Info/People/caldwell/papers.html, March 1997.Google Scholar
  4. 4.
    James Caldwell. Moving proofs-as-programs into practice. In Proceedings, 12th IEEE International Conference Automated Software Engineering. IEEE Computer Society, 1997.Google Scholar
  5. 5.
    R. Constable and D. Howe. Implementing metamathematics as an approach to automatic theorem proving. In R.B. Banerji, editor, Formal Techniques in Artificial Intelligence: A Source Book. Elsevier Science Publishers (North-Holland), 1990.Google Scholar
  6. 6.
    Robert L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.Google Scholar
  7. 7.
    M. Davis and J. Schwartz. Metamathematical extensibility for theorem verifiers and proof checkers. Technical Report 12, Courant Institute of Mathematical Sciences, New York, 1977.Google Scholar
  8. 8.
    Michael J. C. Gordon and Tom F. Melham. Introduction to HOL. Cambridge University Press, 1993.Google Scholar
  9. 9.
    John Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995.Google Scholar
  10. 10.
    Susumu Hayashi. Singleton, union, and intersection types for program extraction. In Proceedings of the International Conference on Theoretical Aspects of Computer Software TACS'91, volume 526 of Lecture Notes in Computer Science, pages 701–730, Berlin, 1991. Springer Verlag.Google Scholar
  11. 11.
    Susumu Hayashi and Hiroshi Nakano. PX: A Computational Logic. Foundations of Computing. MIT Press, Cambridge, MA, 1988.Google Scholar
  12. 12.
    M. Hedberg. Normalising the associative law: An experiment with Martin-Löf's type theory. Formal Aspects of Computing, 3:218–252, 1991.zbMATHCrossRefGoogle Scholar
  13. 13.
    Stephen C. Kleene. Introduction to Metamathematics. van Nostrand, Princeton, 1952.Google Scholar
  14. 14.
    J. Leszczylowski. An experiment with Edinburgh LCF. In W. Bibel and R. Kowalski, editors, 5th International Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 170–181, New York, 1981. Springer-Verlag.Google Scholar
  15. 15.
    C. Paulin-Mohring and B. Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15(5–6):607–640, 1993.zbMATHMathSciNetGoogle Scholar
  16. 16.
    Lawrence Paulson. Proving termination of normalization functions for conditional expressions. Journal of Automated Reasoning, 2:63–74, 1986.zbMATHMathSciNetCrossRefGoogle Scholar
  17. 17.
    N. Shanker. Towards mechanical metamathematics. Journal of Automated Reasoning, 1(4):407–434, 1985.MathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • James L. Caldwell
    • 1
  1. 1.Department of Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations