Symbolic Logic Problem-Solving Software
For The Macintosh

Bertrand is now FREEWARE and OPEN SOURCE. I encourage programmers to improve Bertrand and/or port it to other systems, particularly OS X native. For information on how to obtain the source code in CodeWarrior format, please contact me at

Using a decomposition/instantiation algorithm inspired by the "consistency tree" method found in Leblanc and Wisdom's textbook "Deductive Logic", Bertrand solves sets of first-order symbolic logic statements (subject-identity supported) for satisfiability (consistency), validity, and equivalence. It also checks single statements for "logical truth" and "logical falsity," and produces truth-tables for single truth-functional statements.

During the solution process, Bertrand issues "status reports" which give the user insight into the method by which Bertrand constructs the tree that provides a solution to the problem. These status reports can be stepped through one at a time, or they can be turned off entirely to speed up the solution process.

Once Bertrand has solved a given problem, the tree constructed in the process is displayed in a scrolling window. A summary of results is given in a separate window. If applicable, a verifying (or falsifying) truth-value assignment to relevant atomic statements is provided.

Trees and truth tables can be printed or saved, as can the premises alone. The branches of each tree can be rearranged by dragging them with the mouse pointer; this enables trees to be arranged so as to fit within the indicated printed page margins.

Detailed information on any statement in a tree (including its logical parent, its physical parent, its physical children, its main connective or "operator," and much more) can be obtained by double-clicking on the statement.

Three levels of optimization are available, trading between the shortness of the tree and the length of time needed to produce it.

Many help screens are available, covering everything from the keyboard location of logical symbols to simple symbolization schemas for the beginner.

Bertrand is a "FAT" application which runs in native mode on both PowerPC and 68xxx Macs. It has been tested on System 9.2.2 and in "Classic mode" on OS X, but should be compatible with systems dating back to 8.1 (and perhaps further).

Improvements in current version 1.8: Bertrand now can solve problems in the background. The user can freely access other programs, and work with all other aspects of Bertrand (including saving and printing files), while it is solving a problem. Optimization levels can now be changed "on the fly". Added "Branches Closed" line in the Routine Window. Fixed bug that caused premise files saved out of opened tree files to cause a file system error when opened. Many other internal improvements. Tested on OS 9.2.2 and 10.1 (in Classic mode).

Improvements in version 1.7: Added a user-settable "halting factor" and improved the way Bertrand interprets trees in which the halting factor comes into play. Significantly increased algorithm speed (up to 10 times on trees with many branches, especially with Optimization off). Fixed bug that caused Bertrand sometimes to crash on trees with more than 256 branches. Finally, while Bertrand is still shareware, new users no longer need to obtain a registration code in order to print and save problems.

Click here for a graphic tour of Bertrand.

Go to the Bertrand Download Page.