CAL: A Computer Assisted Learning System for Computation and Logic

摘要

In this paper, we describe a computer system CAL which assists students' understanding of a lecture course in logic and computation. We introduce a new foundational theory of expressions, which is inspired by the theory of expressions due to Martin-Loef [6], and use the expressions determined by the theory to implement various syntactic objects in CAL. We also introduce the concept of derivation game, and show that various logical and computational systems given in the lecture course can be defined uniformly by derivation games.