A logical machine or logical abacus is a tool containing a set of parts that uses energy to perform formal logic operations through the use of truth tables. Early logical machines were mechanical devices that performed basic operations in Boolean logic. The principal examples of such machines are those of William Stanley Jevons (logic piano),[1][2] John Venn,[3] and Allan Marquand.[4][5]
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.