Research Group Logo CS Dept.
Formal Methods and Deduction
Prof. Dr. J. Avenhaus

The DISCOUNT system

The DISCOUNT system (DIStributed COmpletion UsiNg Teamwork) is a distributed theorem prover for pure unit-equality problems that uses the unfailing Knuth-Bendix completion procedure as basic calculus and the teamwork method as distribution concept.
DISCOUNT features many different selection strategies for critical pairs that are highly parameterized. The criteria used by the different strategies range from statistical ones over goal-oriented ones to strategies that use learned prior proof experience (see also our project Learning of search heuristics for theorem provers). By using teamwork, these various strategies can cooperatively work together in finding a proof to a given problem.
Impressum RG Formal Methods and Deduction Department of Informatics Technical University of Kaiserslautern Valid HTML 4.01!

Last Update: Wednesday, 26-Oct-05 08:59:21 GMT