clUB VI:

Sommersemester 2005
Grigori Mints (Stanford): Computerized Exercises to a Course of First Order Logic

We describe a software package and a web server allowing several formats of administering exercises to students and automated answer checking using three computer programs: OTTER, MACE and PRESBURGER. Currently available exercises cover the material corresponding to sections 2.1-2.3 of the textbook by H. Enderton and to a certain degree the Chapter 1. The section 2.4 (Deductive Calculus) can be easily covered by existing software for natural deduction (Fitch or Epgy Proof Editor). Remaining section 2.5 (Soundness and Completeness Theorems) presents a challenge for next stages of the project.

A part of the challenge is discovering new efficiently decidable classes of formulas.


Last changed: June 21st, 2005