Isabelle/HOL as a Meta-Language for Teaching Logic.
Asta Halkjær FromJørgen VilladsenPatrick BlackburnPublished in: ThEdu@IJCAR (2020)
Keyphrases
- natural deduction
- intuitionistic logic
- theorem prover
- inference rules
- cut elimination
- higher order logic
- predicate calculus
- theorem proving
- meta level
- sequent calculus
- online learning
- language learning
- formal theory
- formal language
- operational semantics
- computer programming
- natural language
- dynamic logic
- learning process
- learning analytics
- high school
- first order logic
- programming language
- linear temporal logic
- formal methods
- proof theory
- linear logic
- predicate logic
- e learning
- cooperative learning
- learning environment