Strategic construction of Fitch-style proofs
Studia Logica 60 (1):45-66 (1998)
| 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. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,865 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesJ. B. Kennedy (1995). On the Empirical Foundations of the Quantum No-Signalling Proofs. Philosophy of Science 62 (4):543-560.
Jeremy Avigad (2006). Mathematical Method and Proof. Synthese 153 (1):105 - 159.
R. B. J. T. Allenby (1997). Numbers and Proofs. Copublished in North, South, and Central America by John Wiley & Sons Inc..
Sachio Hirokawa, Yuichi Komori & Misao Nagayama (2000). A Lambda Proof of the P-W Theorem. Journal of Symbolic Logic 65 (4):1841-1849.
Neil Tennant (2009). Revamping the Restriction Strategy. In Joe Salerno (ed.), New Essays on the Knowability Paradox. Oxford University Press.
Wilfried Sieg & John Byrnes (1998). Normal Natural Deduction Proofs (in Classical Logic). Studia Logica 60 (1):67-106.
Dale A. Miller (1987). A Compact Representation of Proofs. Studia Logica 46 (4):347 - 370.
N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads0Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
