What is Scunak?

Scunak is a small, standalone, independent system for formalizing mathematics implemented in Common Lisp and developed by Chad E Brown. One can view Scunak essentially as a program supporting a logical framework "just strong enough" to support natural versions of formal set theory. Scunak is like Automath (see also Freek Wiedijk's fast Automath checker) or Twelf in the sense that the user creates a signature of constants (corresponding to basic concepts and axioms) and definitions (corresponding to defined concepts and theorems with proofs). Like Coq, Scunak provides support for interactively creating proof objects. Also, though one is free to declare constants and definitions for whatever mathematical foundations one wants, Scunak does include built in support for signatures which include certain set theoretic concepts. So, Scunak is unlike Automath or Twelf in that set theory signatures have direct support in the system.

Scunak is also similar to Mizar in many respects. One can reasonably see Scunak as providing a potential language for proof objects for Mizar. In this respect, Scunak is close to the (as far as I know) non-existent system Conproof by Freek Wiedijk.

Four goals were the most important in the design of Scunak:

Formal Correctness: The proofs should be formally checkable as in the deBruijn criterion. The notion of correctness must be simple enough that independent parties can easily implement a checker sufficient to verify the proofs.

Naturality: The mathematics should be represented in a natural way, similar (up to isomorphism) to what appears in mathematics texts. This includes being able to extend the language using definitions and reasonable support for partial functions such as f(x) = 1/x.

Retrievability: Retrieving theorems by content rather than by name or index number must be possible. That is, if we state an instance of a theorem in Scunak's library, then Scunak should be able to find the theorem.

Automation: Some reasonable degree of automated reasoning for proving theorems in the logic should be available.

Among these four criteria, only formal correctness can be claimed at the moment. The rest are work in progress

During the initial stages of its development, Scunak was used to verify a textbook proof (see the paper by Chad E Brown in MKM 2006) which was studied as part of the VeriMathDoc project. This simple textbook proof is included with the distribution as a latex file which can be verified by Scunak. Also included are various latex files of the same proof but with errors (for example, this latex file) for which Scunak can find the error.

Scunak was also able to act as a basic tutor on examples (basic properties of sets and binary relations) from two Wizard of Oz experiments performed as part of the DiaLog project (see the Scunak Manual).

Scunak Downloads:

Scunak 1.0 Scunak 1.0 was released in 2006 and is the only official release to date. It includes different formulations of axiomatic set theory, Kuratowski pairs, function spaces, etc.

Scunak 1.0 runs under Allegro common lisp or clisp.

Scunak Related Publications

Chad E. Brown. Verifying and Invalidating Textbook Proofs using Scunak. Mathematical Knowledge Management, MKM 2006. Wokingham, England. Pages 110-123, 2006.

Chad E. Brown. Encoding Functional Relations in Scunak. LFMTP 2006.

Chad E. Brown. Combining Type Theory and Untyped Set Theory. IJCAR 2006, Seattle, Washington, Pages 205-219, 2006.

Chad E. Brown. Scunak Users Manual. 2006

Chad E Brown. Dependently Typed Set Theory. SEKI-SWP-2006-03

For questions about Scunak, contact Chad E Brown at cebrown at ags dot uni dot sb dot de