Adding ordered rewrite system and conditional rewriting?

[NotBad4U]

I have investigated the reconstruction of arithmetic proofs from Alethe.
For now, I want to try to reconstruct only the steps that provide the coefficients for the simplex.

Example:
Here is the algorithm used to check the unsatisfiability of an inequality:

Here is an example to illustrate the behavior of the la_generic rule:

(step t10 (cl (not (> (f a) (f b))) (not (= (f a) (f b)))) :rule la_generic :args (1.0 -1.0))

The clause (cl) of step t10 is the disjunction not ( (f a) > (f b) ) \/ not( (f a) ≈ (f b)), we apply the algorithm above.

We apply step 2 which applies an n-ary Morgan law,
not ( (f a) > (f b) /\ (f a) ≈ (f b) )

We will verify that the formula ((f a) > (f b) /\ (f a) ≈ (f b)) is unsatisfiable, We apply step 3 of the algorithm:
we obtain (f a) - (f b) > 0 /\ (f a) - (f b) ≈ 0.

As the example is on real numbers (rule la_generic and not lia_generic) we can skip step 4.
Finally, we apply step 5 where we multiply all the conjunctions by the coefficients [1.0 -1.0] and we sum everything.
We obtain (f a) - (f b) > 0 /\ - (f a) + (f b) ≈ 0 after multiplying but the coefficients.

Then we add up the whole
(f a) - (f b) + -(f a) + (f b) > 0 + 0 [Note that this calculation requires AC reasoning]

Finally, we derive the contradiction 0 > 0
■

I think we can try to formalize this computing fully in Lambdapi. However, the computation requires to be able to reason modulo AC. The paper [1] indicates that it is possible to orient equations such as:

• x * y ≈ y * x
• (x * y) * z ≈ x * (y * z)
  if we can put a monotonic order on the terms that is total on the ground terms.

We would therefore have

• (x * y) * z > x * (y * z)
• x * y > y * x if x > y
• (x * y) * z > (y * x) * z. if x > y

We could have the same normal form for an expression and a permutation of this expression.
We will have to try to find an order that would put x and its negation side by side to be able to eliminate them by a rewriting rule e.g. rule x + (-x) ↪ 0.

This method will require adding ordered rewritings and conditional rewriting to Lambdapi.
Does this approach seem reasonable?

Moreover, I think that could also solve also the problem of AC reasoning for permutations of terms in n-ary operators e.g. disjunctions.

---

[1] Martin, U., Nipkow, T. (1990). Ordered rewriting and confluence. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990.