Professor Austen
Clark
Department of Philosophy
University of
Connecticut
Storrs, CT 06269-2054 USA
email: austen.clark<at>uconn.edu
(Spelled out to discourage machine harvesting.)
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.
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.
Read the license agreement
Read the installation instructions.
Download the software (Bextract.exe, a self-extracting file, 273k)
The software in a zip file (in case your firewall does not like exe's. (Bertie3.zip, 172k)
Read some notes on getting started.
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.
Read the license agreement
Read the installation instructions.
Download the software (Textract.exe, a self-extracting file, 269k)
The software in a zip file (in case your firewall does not like exe's. (Twootie.zip, 169k)
Read some notes on getting started.
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.
Look at the readme file.
Download the Windows version of the executable (twoocon.exe) plus problem files (90k).
Download the Linux version of the executable, plus problem files (98k).
Download the source code for Linux and/or Windows (pascal files, a dpr file, problem files) (151k).
Download the source code for Turbo Pascal 5.5 (has minor edits; see readme) (150k).
The self-paced logic project.
The full source code page for Bertie3 and Twootie.
Revised October 2005.
Austen Clark's homepage.
The Philosophy Department homepage