démonstrateur de théorème

CONT: The exploration of the search space (i.e. the proof model) is managed by a theorem prover ... Starting from the data representing the problem hypotheses, the prover produces ... all the facts that can be deduced from the theory.
CONT: The counterexample found above was found by a heuristic filter to the theorem prover called the conjecture disprover.