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.
Similar content being viewed by others
References
Fitch, F. B., Symbolic Logic: An Introduction, Ronald (1952).
Fitting, M., First-Order Logic and Automated Theorem Proving, Springer-Verlag (1990).
JaŚkowski, S., 'On the rules of suppositions in formal logic', Studia Logica I (1934).
Pelletier, F. J., Further developments in THINKER: An automated theorem prover, Technical Report TR-ARP-16/87, Australian National University (1987).
Portoraro, F. D., 'Designing and implementing finite structures in Symlog', Philosophy and the Computer, L. Burkholder editor, 229-234, Westview (1992).
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).
Portoraro, F. D., Natural Deduction in Peano Arithmetic (Addendum to Logic with Symlog: Learning Symbolic Logic by Computer), Prentice-Hall (1994).
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).
Prawitz, D., Natural Deduction: A Proof Theoretical Study, Almqvist & Wiksell, Stockholm (1965).
Sieg, W., Intercalation Calculi for Classical Logic, Report CMU-PHIL 46, Department of Philosophy, Carnegie-Mellon University (1994).
Sieg, W., and J. Byrnes, Normal Natural Deduction Proofs (in classical logic), Report CMU-PHIL 74, Department of Philosophy, Carnegie-Mellon University (1996).
Sieg, W., and B. Kauffmann, Unification for Quantified Formulae, Report CMU-PHIL 44, Department of Philosophy, Carnegie-Mellon University (1993).
Sieg, W., and R. Scheines, 'Searching for proofs (in sentential logic)', Philosophy and the Computer, L. Burkholder editor, 137-159, Westview (1992).
Siekmann, J. H., 'An introduction to unification theory', Formal Techniques in Artificial Intelligence, 369-424, Elsevier Science Publishers, North-Holland (1990).
StÅlmarck, G., 'Normalization theorems for full first order classical natural deduction', JSL Vol. 56,No. 1 (1991).
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).
Szabo, M. E., The Collected Papers of Gerhard Gentzen, M. E. Szabo editor, 68-131, North-Holland (1969).
Author information
Authors and Affiliations
Rights 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
Issue Date:
DOI: https://doi.org/10.1023/A:1005087316935