Suppose you want to quickly test the validity of a certain argument. With Bertrand, you simply select "New" from the file menu-
Select "Validity" from the Problem Type window-
Type in your premises and conclusion (here there is only one premise, but you can have up to 256)-
Watch while the program works (in this case, for only a second)-
Note the Status Reports area. This allows you to follow the program's "reasoning" as it creates the tree that solves your problem (see below for details). Hit "Return" to see the tree and the solution-
Of course, in this case, since the argument is invalid, you might like to see the (in this case partial) truth-value assignment to atomic statements on which the premise is true and the conclusion is false; just click on the "Assignment" button to view this-
Bertrand offers three levels of optimization, trading off between speed (maximized at "Off") and shortness of trees (maximized at "Strong").
The Status Reports option allows the user to watch Bertrand's "reasoning" process as it occurs. You can turn this feature off to maximize speed of solution, or "step" through the solution process one move at a time. The information reported in the status reports can be either basic (just the main steps of the solution algorithm), or more detailed (more information on the algorithm's routines).
Click here to view some of Bertrand's Bells and Whistles.
Go to Bertrand Download Page