The Bertie/Twootie Home Page

Professor Austen Clark
Department of Philosophy
University of Connecticut
Storrs, CT 06269-2054 USA
email: austen.clark<at>
(Spelled out to discourage machine harvesting.)

Three programs for students of symbolic logic

Bertie3 and Twootie 2 are programs that allow students to check their solutions in natural deduction or true trees respectively. Students who practice with the programs get much better at applying the rules of such systems. Both programs are DOS programs, but they will run in a DOS window on machines running Windows (95 and up). No MacIntosh versions are available.
In contrast, the third program (twoocon) is a native Windows program, and it also compiles and runs in Linux. It is a console (or command-line) version of the parser and inference engine of Twootie 2. The source code for it (and the other programs) is available. If you are interested in doing some open-source programming, please check it out.
All of these programs are copyright (c) by Austen Clark, and distributed as "free" or "open source" programs under the provisions of the GNU General Public License. All three are provided as-is, without any warranty of any kind, expressed or implied. Use them at your own risk.

BERTIE3: A proof checker for natural deduction in sentential and predicate logic.

Checks the correctness of any proof using the rule system of Bergmann, Moor, and Nelson, The Logic Book. The program is unique among proof checkers in its use of "templates". These can be generated by mentioning a rule name, edited, and filled in from the bottom up as details emerge. These encourage good strategy in proof construction. Four sets of stored problems are provided with the program. Instructors or students can also create and store their own problems and problem sets, answers to which the program can check. The stored problem sets have sample answers.

TWOOTIE 2.1: A tool for exploring truth trees in sentential and predicate logic.

Checks the correctness of "truth trees" or semantic tableaux, using the rule systems of Bergmann, Moor, and Nelson, The Logic Book, or of Richard Jeffrey, Formal Logic: Its Scope and Limits. This program contains an inference engine which it can use to generate answers to arbitrary problems, as well as to generate hints. It comes with some stored problem sets and allows users to construct and store problem sets of their own. The program can print trees (answers to test problems, for example) in an attractive format.

Twoocon 0.9: A console version of the parser and inference engine of Twootie 2.

The first fruit of freeing the source code of Twootie. Twoocon version 0.9 implements the core functions of Twootie 2, including the full inference engine for predicate logic with identity, which it can use to solve arbitrary problems. The source code will compile and run in either Windows or Linux. The current version is however just a "console" (or command-line) program, aimed at optimizing the computations for big trees, and making it easy to display internals of the data structures. It will be of interest primarily to programmers, instructors, and advanced students. The license agreement is the same as for the other two programs.

Some other links

Revised October 2005.

Austen Clark's homepage.

The Philosophy Department homepage