A distributed and learning equational prover DISCOUNT. 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, reuslts 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 entrant.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei: Cooperating proof attempts (2015)
- Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C.: Machine learning for first-order theorem proving (2014)
- Ma, Jun; Li, Wenjiang; Ruan, Da; Xu, Yang: Filter-based resolution principle for lattice-valued propositional logic LP$(X)$ (2007)
- Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
- Kutsia, Temur: Equational prover of THEOREMA (2003)
- Denzinger, Jörg; Schulz, Stephan: Automatic acquisition of search control knowledge from multiple proof attempts. (2000)
- Denzinger, Joerg; Kronenburg, Martin; Schulz, Stephan: A distributed and learning equational prover DISCOUNT. (1997) ioport