A Connectionist Approach for Learning Search-Control Houristics for Automated Ded

This Doctoral Thesis presents an approach for improving the search process of automated deduction systems by learning from previous experiences. Though the high potential of machine learning and statistical techniques for automated deduction was acknowledged in the early 70s, that is in the early days of deduction, only in recent years practical approaches have been developed. The thesis reviews the most important approaches and identifies fundamental problems and weaknesses. For the first time the problem arising from the existence of several different proofs for one proof problem is recognized, and a convincing solution is presented. Besides the progress achieved for the field of learning for automated deduction which is also demonstrated in experiments, this thesis as a side-effect presents a result with much broader impact. A connectionist approach for solving prediction and classification tasks on structured objects (labelled directed acyclic graphs) of arbitrary size is developed, and experimental results demonstrate its high potential. Thus an answer to one of the most important and challenging open questions in the connectionist community is provided. To a certain degree this work has already established a new research field: adaptive structure processing with connectionist methods. Successful applications in chemistry and data mining can be expected in the near future.