A Programming Notation for Tactical Reasoning

  • David A. Schmidt
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


A notation for expressing the control algorithms (subgoaling strategies) of natural deduction theorem provers is presented. The language provides tools for building widely known, fundamental theorem proving strategies and is independent of the problem area and inference rule system chosen, facilitating formulation of high level algorithms that can be compared, analyzed, and even ported across theorem proving systems. The notation is a simplification and generalization of the tactic language of Edinburgh LCF. Examples using a natural deduction system for propositional logic are given.


Inference Rule Propositional Logic Theorem Prove Natural Deduction Rule Scheme 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. (And).
    Andrews, P.B. Transformaing matings into natural deduction proofs. 5th Conference on Automated Deduction, Les Arcs, France, 1980, LNCS 87, pp. 281–292.Google Scholar
  2. (Ble).
    Bledsoe, W.W., and Tyson, M. The UT interactive theorem prover. Memo ATP-17, Mathematics Dept., University of Texas, Austin, 1975.Google Scholar
  3. (Boy).
    Boyer, R.S., and Moore, J.S. A Computational Logic. Academic Press, New York, 1979.zbMATHGoogle Scholar
  4. (Cha).
    Chang, C., and Lee, R.E. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.zbMATHGoogle Scholar
  5. (Coh).
    Cohen, P.R., and Feigenbaum, E.A., eds. The Handbook of Artificial Intelligence, Vol. 3. Pittman, New York, Ch. 12.Google Scholar
  6. (Con).
    Cohn, A. The equivalence of two semantic definitions: a case study in LCF. Report CSR-76-81, Computer Science Dept., University of Edinburgh, Scotland, 1981.Google Scholar
  7. (CoM).
    Cohn, A., and Milner, R. On using Edinburgh LCF to prove the correctness of a parsing algorithm. Report CSR-113-82, Computer Science Dept., University of Edinburgh, Scotland, 1982.Google Scholar
  8. (Cos).
    Constable, R.L. Proofs as programs: a synopsis. Information Proc. Letters 16-3 (1983) 105–112.CrossRefzbMATHGoogle Scholar
  9. (Got).
    Gordon, M., Milner, R., and Wadsworth, C. Edinburgh LCF. LNCS 78, Springer-Verlag, Berlin, 1979.CrossRefzbMATHGoogle Scholar
  10. (Gut).
    Guttag, J. Notes on type abstraction. IEEE Trans. on Software Engg. SE-6-1 (1980) 13–23.Google Scholar
  11. (Hoa).
    Hoare, C.A.R. An axiomatic basis for computer programming. Comm. ACM 12 (1969) 576–580, 583.CrossRefzbMATHGoogle Scholar
  12. (Lem).
    Lemmon, E.J. Beginning Logic. Nelson, London, 1965.zbMATHGoogle Scholar
  13. (Les).
    Leszczyłowski, J. An experiment with Edinburgh LCF. 5th Conference on Automated Deduction, Les Arcs, France, 1980, LNCS 87, pp. 170–181.Google Scholar
  14. (Mon).
    Monahan, B. Ph.D. thesis, University of Edinburgh, forthcoming.Google Scholar
  15. (Nor).
    Nordström, B. Programming in constructive set theory: some examples. ACM Conf. on Functional Programming Languages and Computer Architecture, Portsmouth, N.H., 1981, pp. 141–153.Google Scholar
  16. (Plo).
    Plotkin, G. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Dept., University of Aarhus, Denmark, 1981.Google Scholar
  17. (Pra).
    Prawitz, D. Natural Deduction. Almquist and Wiksel, Stockholm, 1965.zbMATHGoogle Scholar
  18. (Rob).
    Robinson, J.A. Logic:Form and Function. Edinburgh Univ. Press, Edinburgh, 1979.Google Scholar
  19. (Sup).
    Suppes, P. Introduction to Logic. Van Nostrand, Princeton, 1957.zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • David A. Schmidt
    • 1
  1. 1.Computer Science DepartmentEdinburgh UniversityEdinburghScotland

Personalised recommendations