Class & Int proof checkers

Class and Int are proof checkers for classical and intuitionistic logics respectively. That means they are computer programs that check mathematical proofs for its correctness.

The authors of the systems are Yuri Vtorushin (E-Mail: urchick at mail dot ru) and Oleg Okhotnikov (E-Mail: oleg.okhotnikov at gmail dot com).

We use Class and Int programs on seminars with students in courses "Mathematical logics and algorithm theory", "Artificial inlelligence" etc.

Class 1.0 and Int 1.0 are dedicated for reasoning verification in natural deduction system of single-typed first-order logic language. Class 2.0 and Int 2.0 are for many-typed logic.

There are syntax description and semantic rules for version 1.0.

Proof checkers are command-line tools and used as follows:

class -f:filename.cls
int -f:filename.int

or:

class <filename.cls
int <filename.int

there filename.cls and filename.int are names of text files to verify for.

This site is best viewed with Opera and Firefox

This site last updated: 8 november 2007

(This site is under construction)