View in EDS

Teaching Logic Using a State-of-the-Art Proof Assistant

Saved in:
Bibliographic Details
Title: Teaching Logic Using a State-of-the-Art Proof Assistant
Language: English
Authors: Hendriks, Maxim, Kaliszyk, Cezary, van Raamsdonk, Femke, Wiedijk, Freek
Source: Acta Didactica Napocensia. 2010 3(2):35-48.
Availability: Babes-Bolyai University. Kogainiceanu 1, Cluj-Napoca, 400084 Romania. e-mail: submit_adn@yahoo.com; Web site: http://adn.teaching.ro
Peer Reviewed: Y
Page Count: 14
Publication Date: 2010
Document Type: Journal Articles
Reports - Descriptive
Education Level: Higher Education
Postsecondary Education
Descriptors: Logical Thinking, Teaching Methods, Validity, Undergraduate Students, Computer Science, Educational Technology, Databases, Problem Solving, Computer Uses in Education, Foreign Countries, Computer Science Education
Geographic Terms: Netherlands
ISSN: 2065-1430
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/.
Abstractor: As Provided
Number of References: 23
Entry Date: 2015
Accession Number: EJ1056118
Database: ERIC
FullText Text:
  Availability: 0
CustomLinks:
  – Url: https://eric.ed.gov/contentdelivery/servlet/ERICServlet?accno=EJ1056118
    Name: ERIC Full Text
    Category: fullText
    Text: Full Text from ERIC
Header DbId: eric
DbLabel: ERIC
An: EJ1056118
AccessLevel: 3
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Teaching Logic Using a State-of-the-Art Proof Assistant
– Name: Language
  Label: Language
  Group: Lang
  Data: English
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Hendriks%2C+Maxim%22">Hendriks, Maxim</searchLink><br /><searchLink fieldCode="AR" term="%22Kaliszyk%2C+Cezary%22">Kaliszyk, Cezary</searchLink><br /><searchLink fieldCode="AR" term="%22van+Raamsdonk%2C+Femke%22">van Raamsdonk, Femke</searchLink><br /><searchLink fieldCode="AR" term="%22Wiedijk%2C+Freek%22">Wiedijk, Freek</searchLink>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="SO" term="%22Acta+Didactica+Napocensia%22"><i>Acta Didactica Napocensia</i></searchLink>. 2010 3(2):35-48.
– Name: Avail
  Label: Availability
  Group: Avail
  Data: Babes-Bolyai University. Kogainiceanu 1, Cluj-Napoca, 400084 Romania. e-mail: submit_adn@yahoo.com; Web site: http://adn.teaching.ro
– Name: PeerReviewed
  Label: Peer Reviewed
  Group: SrcInfo
  Data: Y
– Name: Pages
  Label: Page Count
  Group: Src
  Data: 14
– Name: DatePubCY
  Label: Publication Date
  Group: Date
  Data: 2010
– Name: TypeDocument
  Label: Document Type
  Group: TypDoc
  Data: Journal Articles<br />Reports - Descriptive
– Name: Audience
  Label: Education Level
  Group: Audnce
  Data: <searchLink fieldCode="EL" term="%22Higher+Education%22">Higher Education</searchLink><br /><searchLink fieldCode="EL" term="%22Postsecondary+Education%22">Postsecondary Education</searchLink>
– Name: Subject
  Label: Descriptors
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Logical+Thinking%22">Logical Thinking</searchLink><br /><searchLink fieldCode="DE" term="%22Teaching+Methods%22">Teaching Methods</searchLink><br /><searchLink fieldCode="DE" term="%22Validity%22">Validity</searchLink><br /><searchLink fieldCode="DE" term="%22Undergraduate+Students%22">Undergraduate Students</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+Science%22">Computer Science</searchLink><br /><searchLink fieldCode="DE" term="%22Educational+Technology%22">Educational Technology</searchLink><br /><searchLink fieldCode="DE" term="%22Databases%22">Databases</searchLink><br /><searchLink fieldCode="DE" term="%22Problem+Solving%22">Problem Solving</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+Uses+in+Education%22">Computer Uses in Education</searchLink><br /><searchLink fieldCode="DE" term="%22Foreign+Countries%22">Foreign Countries</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+Science+Education%22">Computer Science Education</searchLink>
– Name: Subject
  Label: Geographic Terms
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Netherlands%22">Netherlands</searchLink>
– Name: ISSN
  Label: ISSN
  Group: ISSN
  Data: 2065-1430
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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/.
– Name: AbstractInfo
  Label: Abstractor
  Group: Ab
  Data: As Provided
– Name: Ref
  Label: Number of References
  Group: RefInfo
  Data: 23
– Name: DateEntry
  Label: Entry Date
  Group: Date
  Data: 2015
– Name: AN
  Label: Accession Number
  Group: ID
  Data: EJ1056118
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=eric&AN=EJ1056118
RecordInfo BibRecord:
  BibEntity:
    Languages:
      – Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 14
        StartPage: 35
    Subjects:
      – SubjectFull: Logical Thinking
        Type: general
      – SubjectFull: Teaching Methods
        Type: general
      – SubjectFull: Validity
        Type: general
      – SubjectFull: Undergraduate Students
        Type: general
      – SubjectFull: Computer Science
        Type: general
      – SubjectFull: Educational Technology
        Type: general
      – SubjectFull: Databases
        Type: general
      – SubjectFull: Problem Solving
        Type: general
      – SubjectFull: Computer Uses in Education
        Type: general
      – SubjectFull: Foreign Countries
        Type: general
      – SubjectFull: Computer Science Education
        Type: general
      – SubjectFull: Netherlands
        Type: general
    Titles:
      – TitleFull: Teaching Logic Using a State-of-the-Art Proof Assistant
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Hendriks, Maxim
      – PersonEntity:
          Name:
            NameFull: Kaliszyk, Cezary
      – PersonEntity:
          Name:
            NameFull: van Raamsdonk, Femke
      – PersonEntity:
          Name:
            NameFull: Wiedijk, Freek
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 01
              Type: published
              Y: 2010
          Identifiers:
            – Type: issn-electronic
              Value: 2065-1430
          Numbering:
            – Type: volume
              Value: 3
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Acta Didactica Napocensia
              Type: main
ResultId 1