SEMANTIC TREES IN AUTOMATIC THEOREM-PROVING

Abstract

Application of modified version of semantic trees to problem of finding efficient rules of proof for mechanical theorem-proving, from viewpoint of clash resolution using semantic tree for predicate calculus without equality; report on attempts to apply methods of semantic trees to construction of inference systems for predicate calculus with equality.