Skip to main content
Log in

Strategic Construction of Fitch-style Proofs

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

Symlog is a system for learning symbolic logic by computer that allows students to interactively construct proofs in Fitch-style natural deduction. On request, Symlog can provide guidance and advice to help a student narrow the gap between goal theorem and premises. To effectively implement this capability, the program was equipped with a theorem prover that constructs proofs using the same methods and techniques the students are being taught. This paper discusses some of the aspects of the theorem prover's design, including its set of proof-construction strategies, its unification algorithm as well as some of the tradeoffs between efficiency and pedagogy.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Fitch, F. B., Symbolic Logic: An Introduction, Ronald (1952).

  2. Fitting, M., First-Order Logic and Automated Theorem Proving, Springer-Verlag (1990).

  3. JaŚkowski, S., 'On the rules of suppositions in formal logic', Studia Logica I (1934).

  4. Pelletier, F. J., Further developments in THINKER: An automated theorem prover, Technical Report TR-ARP-16/87, Australian National University (1987).

  5. Portoraro, F. D., 'Designing and implementing finite structures in Symlog', Philosophy and the Computer, L. Burkholder editor, 229-234, Westview (1992).

  6. Portoraro, F. D., 'Symlog: Automated advice in Fitch-style proof construction', Automated Deduction-CADE 12, Lecture Notes in Artificial Intelligence, A. Bundy editor, vol. 814, 802-806, Springer-Verlag (1994).

  7. Portoraro, F. D., Natural Deduction in Peano Arithmetic (Addendum to Logic with Symlog: Learning Symbolic Logic by Computer), Prentice-Hall (1994).

  8. Portoraro, F. D., and R. E. Tully, Logic with Symlog: Learning Symbolic Logic by Computer, Prentice-Hall (1994). The software: Symlog ver. 2.0 (1992).

  9. Prawitz, D., Natural Deduction: A Proof Theoretical Study, Almqvist & Wiksell, Stockholm (1965).

    Google Scholar 

  10. Sieg, W., Intercalation Calculi for Classical Logic, Report CMU-PHIL 46, Department of Philosophy, Carnegie-Mellon University (1994).

  11. Sieg, W., and J. Byrnes, Normal Natural Deduction Proofs (in classical logic), Report CMU-PHIL 74, Department of Philosophy, Carnegie-Mellon University (1996).

  12. Sieg, W., and B. Kauffmann, Unification for Quantified Formulae, Report CMU-PHIL 44, Department of Philosophy, Carnegie-Mellon University (1993).

  13. Sieg, W., and R. Scheines, 'Searching for proofs (in sentential logic)', Philosophy and the Computer, L. Burkholder editor, 137-159, Westview (1992).

  14. Siekmann, J. H., 'An introduction to unification theory', Formal Techniques in Artificial Intelligence, 369-424, Elsevier Science Publishers, North-Holland (1990).

    Google Scholar 

  15. StÅlmarck, G., 'Normalization theorems for full first order classical natural deduction', JSL Vol. 56,No. 1 (1991).

  16. Suppes, P., et al., 'Part I. Interactive theorem proving in CAI courses', University-Level Computer-Assisted Instruction at Stanford: 1968–1980, P. Suppes editor, IMSSS, Stanford University (1981).

  17. Szabo, M. E., The Collected Papers of Gerhard Gentzen, M. E. Szabo editor, 68-131, North-Holland (1969).

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

About this article

Cite this article

Portoraro, F.D. Strategic Construction of Fitch-style Proofs. Studia Logica 60, 45–66 (1998). https://doi.org/10.1023/A:1005087316935

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1005087316935

Keywords

Navigation