Teaching logic using a state-of-art proof assistant

dc.creator	Maxim Hendriks
dc.creator	Cezary Kaliszyk
dc.creator	Femke van Raamsdonk
dc.creator	Freek Wiedijk
dc.date	2010-06-01T00:00:00Z
dc.date.accessioned	2015-08-12T11:36:57Z
dc.date.available	2015-08-12T11:36:57Z
dc.identifier	2065-1430
dc.identifier	https://doaj.org/article/7f94b26d134b46f7ada5c91730198ed8
dc.identifier.uri	http://evidence.thinkportal.org/handle/123456789/31403
dc.description	This article describes the system ProofWeb developed for teaching logic to undergraduate computer science students. The system is based on the higher order proof assistant Coq, and is made available to the students through an interactive web interface. Part of this system is a large database of logic problems. This database will also hold the solutions of the students. The students do not need to install anything to be able to use the system (not even a browser plug-in), and the teachers are able to centrally track progress of the students. The system makes the full power of Coq available to the students, but simultaneously presents the logic problems in a way that is customary in undergraduate logic courses. Both styles of presenting natural deduction proofs (Gentzen-style `tree view' and Fitch-style `box view') are supported. Part of the system is a parser that indicates whether the students used the automation of Coq to solve their problems or that they solved it themselves using only the inference rules of the logic. For these inference rules dedicated tactics for Coq have been developed. The system has already been used in type theory courses and logic undergraduate courses. The ProofWeb system can be tried at http://proofweb.cs.ru.nl/.
dc.language	English
dc.publisher	Babes-Bolyai University, Cluj-Napoca
dc.relation	http://adn.teaching.ro/v3n2a4.htm
dc.relation	https://doaj.org/toc/2065-1430
dc.source	Acta Didactica Napocensia, Vol 3, Iss 2, Pp 35-48 (2010)
dc.subject	Logic Education
dc.subject	Proof Assistants
dc.subject	Coq
dc.subject	Web Interface
dc.subject	Natural Deduction
dc.subject	Education (General)
dc.subject	L7-991
dc.subject	Education
dc.subject	L
dc.subject	DOAJ:Education
dc.subject	DOAJ:Social Sciences
dc.subject	Education (General)
dc.subject	L7-991
dc.subject	Education
dc.subject	L
dc.subject	DOAJ:Education
dc.subject	DOAJ:Social Sciences
dc.subject	Education (General)
dc.subject	L7-991
dc.subject	Education
dc.subject	L
dc.subject	Education (General)
dc.subject	L7-991
dc.subject	Education
dc.subject	L
dc.subject	Education (General)
dc.subject	L7-991
dc.subject	Education
dc.subject	L
dc.title	Teaching logic using a state-of-art proof assistant
dc.type	article