Studia Logica 60 (1):45-66 (1998)
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||Philosophy Logic Mathematical Logic and Foundations Computational Linguistics|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
On the Empirical Foundations of the Quantum No-Signalling Proofs.J. B. Kennedy - 1995 - Philosophy of Science 62 (4):543-560.
Normal Natural Deduction Proofs (in Classical Logic).Wilfried Sieg & John Byrnes - 1998 - Studia Logica 60 (1):67-106.
Revamping the Restriction Strategy.Neil Tennant - 2009 - In Joe Salerno (ed.), New Essays on the Knowability Paradox. Oxford University Press.
A Lambda Proof of the P-W Theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
Numbers and Proofs.R. B. J. T. Allenby - 1997 - Copublished in North, South, and Central America by John Wiley & Sons.
Added to index2009-01-28
Total downloads12 ( #376,705 of 2,170,078 )
Recent downloads (6 months)1 ( #345,514 of 2,170,078 )
How can I increase my downloads?