Natural Deduction Assistant (NaDeA)

Autor: Villadsen, Jørgen, From, Andreas Halkjær, Schlichtkrull, Anders

Publikováno v: EPTCS 290, 2019, pp. 14-29

We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first pro

Externí odkaz: http://arxiv.org/abs/1904.00618

Natural Deduction and the Isabelle Proof Assistant

Autor: Villadsen, Jørgen, From, Andreas Halkjær, Schlichtkrull, Anders

Publikováno v: EPTCS 267, 2018, pp. 140-155

We describe our Natural Deduction Assistant (NaDeA) and the interfaces between the Isabelle proof assistant and NaDeA. In particular, we explain how NaDeA, using a generated prover that has been verified in Isabelle, provides feedback to the student,

Externí odkaz: http://arxiv.org/abs/1803.01473

Students' Proof Assistant (SPA)

Autor: Anders Schlichtkrull, Jørgen Villadsen, Andreas Halkjær From

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 290, Iss Proc. ThEdu 2018, Pp 1-13 (2019)

The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant. In additio

Externí odkaz: https://doaj.org/article/14d1247fbec74933872e08c9bfe3369e

Multi-Agent Programming Contest 2018—The Jason-DTU Team

Autor: Villadsen, Jørgen, Bjørn, Mads Okholm, From, Andreas Halkjær, Henney, Thomas Søren, Larsen, John Bruntse

Publikováno v: Villadsen, J, Bjørn, M O, From, A H, Henney, T S & Larsen, J B 2020, Multi-Agent Programming Contest 2018—The Jason-DTU Team . in T Ahlbrecht, J Dix & N Fiekas (eds), The Multi-Agent Programming Contest 2018 . Springer, Lecture Notes in Computer Science, vol. 11957, pp. 41-71, The Multi-Agent Programming Contest 2018, Clausthal, Lower Saxony, Germany, 24/09/2018 . https://doi.org/10.1007/978-3-030-37959-9_3

We provide a brief description of the Jason-DTU system, including the overall system design and the tools that we used in the Multi-Agent Programming Contest. We also provide a detailed evaluation of our system. The strengths of our system include dy

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______1202::30f2d2a7abf0ad4673f24d2a09bfe206
https://orbit.dtu.dk/en/publications/3a10d99f-867d-43e0-9f57-50f68ce819f3

Natural Deduction Assistant (NaDeA)

Autor: Andreas Halkjær From, Jørgen Villadsen, Anders Schlichtkrull

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 290, Iss Proc. ThEdu 2018, Pp 14-29 (2019)
Villadsen, J, From, A H & Schlichtkrull, A 2018, ' Natural Deduction Assistant (NaDeA) ', Paper presented at International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18/07/2018-18/07/2018 .
Technical University of Denmark Orbit
Villadsen, J, From, A H & Schlichtkrull, A 2019, ' Natural Deduction Assistant (NaDeA) ', Electronic Proceedings in Theoretical Computer Science, vol. 290, pp. 14–29 . https://doi.org/10.4204/EPTCS.290.2

We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first pro

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::88a0eb3d039660ed626461209300a6dc
http://arxiv.org/abs/1904.00618