> 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.
\--developer's description
DL #1-3 - Bertrand v1.1 (68k, FAT and PPC)
DL #4-5 - Bertrand v1.4 (FAT and PPC)
DL #6-7 - Bertrand v1.6 (68k and PPC)
