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.

References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  2. Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
  3. Schulz, Stephan; Cruanes, Simon; Vukmirović, Petar: Faster, higher, stronger: E 2.3 (2019)
  4. Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
  5. Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei: Cooperating proof attempts (2015)
  6. Schulz, Stephan; Sutcliffe, Geoff: Proof generation for saturating first-order theorem provers (2015)
  7. Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C.: Machine learning for first-order theorem proving (2014)
  8. Korovin, Konstantin: Inst-Gen -- a modular approach to instantiation-based automated reasoning (2013)
  9. Schulz, Stephan: Simple and efficient clause subsumption with feature vector indexing (2013)
  10. Ma, Jun; Li, Wenjiang; Ruan, Da; Xu, Yang: Filter-based resolution principle for lattice-valued propositional logic LP((X)) (2007)
  11. Newborn, Monty; Wang, Zongyan: Octopus: combining learning and parallel search (2004)
  12. Kutsia, Temur: Equational prover of THEOREMA (2003)
  13. Benzmüller, Christoph; Jamnik, Mateja; Kerber, Manfred; Sorge, Volker: Experiments with an agent-oriented reasoning system (2001)
  14. Denzinger, Jörg; Schulz, Stephan: Automatic acquisition of search control knowledge from multiple proof attempts. (2000)
  15. Denzinger, Joerg; Kronenburg, Martin; Schulz, Stephan: A distributed and learning equational prover DISCOUNT. (1997) ioport