Experimental System for Problem Solving

Experimental system for problem solving on the base of logical deduction is described. Natural language texts are the input of the system. Logical inference by sintactic tree method is used. Data base operations for search and keeping theorems were realized in the system. System work is demonstrated for geometry problems. Perspectives of approach are discussed.