| | | B.2.6 counterexample: Generate Counterexample |
counterexample
: counterexample
In proving mode.
A decision procedure may generate for the current proof state
[E] A_1, A_2, ..., A_n |- B_1, B_2, ..., B_m
a counterexample, i.e. an interpretation for the constants declared in the environment E which it believes to satisfy the formula
A_1 /\ A_2 /\ ... /\ A_n /\ ~B_1 /\ ~B_2 /\ ... /\ ~B_m
The counterexample is given as a conjunction of equations c=t respectively c(...)=t for non-Boolean constants/functions c and of atomic propositions p respectively p(...) for Boolean constants/functions (i.e. predicates) p.
The presented counterexample is often verbose and not
very helpful. This counterexample is actually only a part of the
counterexample generated by the decision procedure where (seemingly)
uninteresting conditions have been removed. The generation of the
counterexample may take some time; this process may be interrupted by pressing
the abort button
.
| | | B.2.6 counterexample: Generate Counterexample |