Post by Charlie-Boo
I have 5 nonnegative real number variables: A B C M N
1. A + B + C = 10
2. A <= M <= A + C
3. B <= N <= B + C
4. M + N = 5
5. B < 2
Here;s hg9ow you find the answer -- automatically.
(1) Generate a large random set of values for (A,B,C,M,N).
(2) For each combination, produce a 5-bit value based on the yes/no answer to 1, 2, 3, 4, 5 for that combination.
(3) Sort the 5-bit values (and eliminate redundancies)
(4) For each value produce the corresponding boolean expression; e.g. (1 yes, 2 no, 3 yes, 4 yes, 5 no would yield I and not II and III and IV and not V).
(5) Let E0, E1, E2, ... be the expressions formed as a result. Take their disjunction E = E0 or E1 or E2 ...
(6) Convert this to disjunctive normal form. The result is an expression of the form E = F0 and F1 and F2 and ..., where each F has a form, such as (not I or not II or not III or IV or V).
Each F is a relation that probably holds between the statements; e.g. not I or not II or not III or IV or V is the conditional: (I and II and III -> IV or V).
Establish each statement F0, F1, F2, ... with a theorem prover (or by hand) .. or seek out a counter example by generating more combinations of (A, B, C, M, N).
There is a way to DIRECTLY incorporate a counter-example into an update of the list of F's; but I won't go into it here.
Prover9 (theorem prover)/Mace 4 (model finder) can be used to find proofs and models. https://www.cs.unm.edu/~mccune/mace4/