Discussion:
Equation Dependencies: Which of these equation imply which others?
Add Reply
Charlie-Boo
2017-08-11 14:33:50 UTC
Reply
Permalink
Raw Message
I have 5 nonnegative real number variables: A B C M N
< = means less than or equal to, < means less than

1. A + B + C = 10
2. A <= M <= A + C
3. B <= N <= B + C
4. M + N = 5
5. B < 2

Which sets of these 5 equations imply which other equations (or parts thereof for 2 and 3)?

I need to enforce these and want to eliminate redundancy.

Thanks,

Charlie
Roland Franzius
2017-08-11 16:16:54 UTC
Reply
Permalink
Raw Message
Post by Charlie-Boo
I have 5 nonnegative real number variables: A B C M N
< = means less than or equal to, < means less than
1. A + B + C = 10
2. A <= M <= A + C
3. B <= N <= B + C
4. M + N = 5
5. B < 2
Which sets of these 5 equations imply which other equations (or parts thereof for 2 and 3)?
I need to enforce these and want to eliminate redundancy.
Reduces automatically to

((N < 2 && B <= N && C >= 5 - B + N) || (N >= 2 && B < 2 &&
C >= 5 - B + N)) && M == 5 - N && A == 10 - B - C
--
Roland Franzius
Mike Terry
2017-08-11 18:07:15 UTC
Reply
Permalink
Raw Message
Post by Charlie-Boo
I have 5 nonnegative real number variables: A B C M N
< = means less than or equal to, < means less than
1. A + B + C = 10
2. A <= M <= A + C
3. B <= N <= B + C
4. M + N = 5
5. B < 2
Which sets of these 5 equations imply which other equations (or parts thereof for 2 and 3)?
I need to enforce these and want to eliminate redundancy.
Thanks,
Charlie
The second halves of (2) and (3) would seem to be redundant, given all
the rest. This brings you down to 5 tests.

Regards,
Mike.
r***@gmail.com
2017-08-11 22:09:42 UTC
Reply
Permalink
Raw Message
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/
Loading...