Bertrand is both an educational aid for students of logic and a practical tool for philosophers, logicians, computer programmers, and mathematicians. Using an algorithm inspired by the "consistency tree" method found in Leblanc and Wisdom's textbook Deductive Logic, Bertrand proceeds by decomposition and instantiation to solve first-order predicate logic statements for satisfiability, validity, equivalence, logical truth, and logical falsity. Subject-equality is supported. The program also produces truth tables for truth-functional sentences.
System 7.1 or later