ISSN:
1573-0670
Keywords:
automated theorem proving
;
competition
;
DISCOUNT
;
distributed theorem proving
;
reactive planning
;
learning
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract The DISCOUNT system is a distributed equational theorem prover based on the teamwork method for knowledge-based distribution. It uses an extended version of unfailing Knuth–Bendix completion that is able to deal with arbitrarily quantified goals. DISCOUNT features many different control strategies that cooperate using the teamwork approach. Competition between multiple strategies, combined with reactive planning, results in an adaptation of the whole system to given problems, and thus in a very high degree of independence from user interaction. Teamwork also provides a suitable framework for the use of control strategies based on learning from previous proof experiences. One of these strategies forms the core of the expert global_learn, which is capable of learning from successful proofs of several problems. This expert, running sequentially, was one of the entrants in the competition (DISCOUNT/GL), while a distributed DISCOUNT system running on two workstations was another en trant.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1005879229581
Permalink