Cooperation in heterogeneous theorem prover networks (Diss., Univ. Kaiserslautern) (Q2726294)

The problem addressed in this dissertation about one of the most interesting area in artificial intelligence, automated theorem proving, is : what is needed to compose a set of heterogeneous provers to a team that performs a cooperative search for a proof . The author presents an abstract model in heterogeneous theorem prover networks which consistof arbitrary saturation based and analytical provers. Starting from a set of competitive provers, cooperation is achieved by exchanging information periodically: positive information (represented by clauses) that provers should utilize, and negative information that specifies proof paths that do not appear to be promising. The author examines the combination of bottom-up and top-down reasoning by the cooperation of provers based on the superposition and the connection tableau calculus. Also he integrates specialized concepts by adding equational provers based on the unfailing completion procedure. NEWLINENEWLINENEWLINEThe chapters of the thesis are: Theorem proving in first-order clause logic, Parallel and cooperative deduction, A framework for cooperative heterogeneous theorem proving, Combining superposition provers with loosely coupled heuristics, Coupling proof procedures for the connection tableau calculus, Cooperation between superposition and connection tableau calculi, Integration of equational provers into a cooperative team. NEWLINENEWLINENEWLINEAs the author says, as a result of his studies, three quite different provers, based on resolution, model elimination and Knuth-Bendix completion, were combined and the synergetic effects were demostrated. NEWLINENEWLINENEWLINEThe thesis can serve as instructional material for a course on theorem proving or AI at graduate level.