Cooperation in heterogeneous theorem prover networks (Diss., Univ. Kaiserslautern)
type: Item
instance of: scholarly article
zbMATH Open document ID: 0977.68075
author: Dirk Fuchs
publication date: 2001-07-17T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68-02
zbMATH DE Number: 1620754
zbMATH Keywords: first-order clause logic
zbMATH Keywords: paralel and cooperative deduction
zbMATH Keywords: resolution refutation proofs
zbMATH Keywords: tableau calculus
zbMATH Keywords: provers
MaRDI profile type: Publication
Recommended article: Q4524781
Recommended article: Q4242056
Recommended article: Parallel cooperative propositional theorem proving
Recommended article: Coherence for sharing proof nets
Recommended article: Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
Recommended article: Coherence for sharing proof-nets
Recommended article: Q4246966
Recommended article: Q4282573
Recommended article: A competitive and cooperative approach to propositional satisfiability
title: Cooperation in heterogeneous theorem prover networks (Diss., Univ. Kaiserslautern)
published in: DISKI. Dissertationen zur Künstlichen Intelligenz
review text: 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.
reviewed by: Doina Tatar
description: scientific article; zbMATH DE number 1620754