Semantic tree method - historical perspective and applications

Abstract

The method of semantic tablaux or semantic tree is a very well known method in logic. Everyone who had ever learned logic knows basic rules and applications of this method. In the paper special attention is drawn to the history of this method as a part of the history of computers (especially of the history of mechanization of reasoning) and its applications. The method itself is presented for the classical propositional calculus and predicate calculus.