CODEWITHSUNDEEP
pythonmatlabprolog
user3417588
user3417588

Reputation: 13

Check if a system of inequalities entails another system of equalities?

I have a system of inequalities, but the problem is all of the terms in the system are unassigned variables (edit: all variables are representing natural numbers). Like I want to give the system rules like:

    a + b >= f + h
    f + b >= d + e
    d + b >= a + c

and then ask the system if a query like 

    d + e >= f + g

must be true. Does anyone know how to do this in matlab or python or even prolog?

Upvotes: 1

Views: 109

Answers (1)

mat
mat

Reputation: 40768

As you have clarified, you are reasoning over natural numbers.

The particular case you show is an example of Presburger arithmetic, which is a decidable fragment of arithmetic. There are several theorem provers for Presburger arithmetic available, written in Prolog and also in other languages.

Using such provers, you can for example show that the fourth equality is not entailed by the preceding three:

?- valid(a + b >= f + h /\
         f + b >= d + e /\
         d + b >= a + c ==>
         d + e >= f + g).
false.

Here is an explicit counterexample:

?- solution(a + b >= f + h /\
            f + b >= d + e /\
            d + b >= a + c /\
            not(d + e >= f + g)).
a=0.
b=0.
f=0.
h=0.
d=0.
e=0.
c=0.
g=1.

Alternatively, with Prolog, you can for example use constraint logic programming over integers or rational numbers, abbreviated as and respectively, to search for counterexamples.

For instance, in the case you show, and using CLP(Q):

?- { A + B >= F + H,
     F + B >= D + E,
     D + B >= A + C,
     D + E < F + G }.
{_1692>0, ...}.

This answer shows (since CLP(Q) is complete) that a counterexample exists over Q, but does not tell us whether the formula is entailed over the integers or natural numbers. However, if this query had failed, then we would have known that no counterexample exists over Q and hence not over N, meaning that the last inequality would indeed be entailed over N.

To search for counterexamples over N, and even over integers, with constraint logic programming, you can use CLP(FD). For example, you can post the constraints that a counterexample must satisfy:

?- A + B #>= F + H #/\
   F + B #>= D + E #/\
   D + B #>= A + C #/\
   #\ (D + E #>= F + G),

You can search for concrete solutions via labeling. However, this requires that all domains be finite. We can start for example with 0..2, and try increasingly larger domains. This strategy is complete: If there is a counterexample, we will find it in this way. If, on the other hand, no counterexample exists, consider that we cannot draw any conclusion regarding the formula's validity from the fact that we have not yet found one.

In this case, we are lucky and soon find several counterexamples:

?- A + B #>= F + H #/\
   F + B #>= D + E #/\
   D + B #>= A + C #/\
   #\ (D + E #>= F + G),
   Vs = [A,B,C,D,E,F,G,H],
   Vs ins 0..2,
   label(Vs).
A = B, B = F, F = H, H = D, D = E, E = C, C = 0,
G = 1,
Vs = [0, 0, 0, 0, 0, 0, 1, 0] ;
A = B, B = F, F = H, H = D, D = E, E = C, C = 0,
G = 2,
Vs = [0, 0, 0, 0, 0, 0, 2, 0] ;
A = F, F = H, H = D, D = E, E = C, C = 0,
B = G, G = 1,
Vs = [0, 1, 0, 0, 0, 0, 1, 0] ;
A = F, F = D, D = E, E = C, C = 0,
B = H, H = G, G = 1,
Vs = [0, 1, 0, 0, 0, 0, 1, 1] ;
A = F, F = H, H = D, D = E, E = C, C = 0,
B = 1,
G = 2,
Vs = [0, 1, 0, 0, 0, 0, 2, 0] .

In summary, I suggest a combination of:

  • theorem provers over Presburger arithmetic
  • CLP(FD)
  • CLP(Q)
  • and possibly further methods

to find counterexamples or proofs of such entailments.

Note that this quickly becomes undecidable in general, but it is decidable over linear formulas.

Upvotes: 1

Related Questions