logical machine

Contemporary logical machines are computer-based electronic programs that perform proof assistance with theorems in mathematical logic. In the 21st century, these proof assistant programs have given birth to a new field of study called mathematical knowledge management.

The earliest logical machines were mechanical constructs built in the late 19th century. William Stanley Jevons invented the first logical machine in 1869, the logic piano. In 1883, Allan Marquand invented a new logical machine that performed the same operations as Jevons' logic piano but with improvements in design simplification, portability, and input-output controls. A logical abacus is constructed to show all the possible combinations of a set of logical terms with their negatives, and, further, the way in which these combinations are affected by the addition of attributes or other limiting words, i.e., to simplify mechanically the solution of logical problems. These instruments are all more or less elaborate developments of the "logical slate", on which were written in vertical columns all the combinations of symbols or letters which could be made logically out of a definite number of terms. These were compared with any given premises, and those which were incompatible were crossed off. In the abacus the combinations are inscribed each on a single slip of wood or similar substance, which is moved by a key; incompatible combinations can thus be mechanically removed at will, in accordance with any given series of premises.