Logo Fachportal Pädagogik -Deutscher BildungsserverDeutscher BildungsberichtBildung in DeutschlandHistorische Bildungsforschung online Deutsches Institut für Internationale Pädagogische Forschung
grün und orangener Balken 1   grün und orangener Balken 3
Logo FIS

FIS Bildung Literaturdatenbank - Vollanzeige

Autoren: Hendriks, Maxim; Kaliszyk, Cezary; Raamsdonk, Femke van; Wiedijk, Freek
Titel: Teaching logic using a state-of-art proof assistant.
Quelle: In: Acta didactica Napocensia, 3 (2010) 2, S. 35-48
Dokument online lesbar. Link öffnet Datei in neuem Fenster.Volltext  Pfeil auf den Link... Link als defekt melden     Pfeil auf den Link... Verfügbarkeit 
Beigaben: Illustrationen
Zusatzinformation: http://proofweb.cs.ru.nl/
Sprache: englisch
Dokumenttyp: online; Zeitschriftenaufsatz
ISSN: 1504-9922; 2065-1430
Schlagwörter: Unterricht; Berufspädagogik; Internet; Informationswissenschaft; Europa; Rumänien
Abstract: 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/. The papers in this number are extended versions of the presentations given at the Second Computer Algebra and Dynamic Geometry Systems in Mathematics Education (CADGME) conference at the University of Linz, Austria, in July 2009. (Orig./DIPF/Hah).
Erfasst von: Externer Selbsteintrag
Update: 2011/1
Verfügbarkeit: Literaturbeschaffung und Bestandsnachweise in Bibliotheken

Standortgebundene Dienste

Wählen Sie eine Institution, um dort die Verfügbarkeit zu prüfen:  



Laut Auskunft der Elektronischen Zeitschriftendatenbank (EZB) ist der Artikel in der Online-Ausgabe der Zeitschrift "Acta didactica Napocensia" kostenlos erschienen



Standortunabhängige Dienste
Bibliotheken, die die Zeitschrift "Acta didactica Napocensia" besitzen:
Link zur Zeitschriftendatenbank (ZDB)

Artikellieferdienst der deutschen Bibliotheken (subito):
Übernahme der Daten in das subito-Bestellformular


Tipps zum Auffinden elektronischer Volltexte als Video-Tutorial


Nachweis posten:

 

Nachweis merken:

 
  

Nachweis exportieren:

 


im gewählten Format an:

Permalink als QR-Code: