Alessio Coltellacci
Alessio Coltellacci
> Example: in your Makefile, add: > > ``` > include lpo.mk > LP_FILES := $(wildcard *.lp) > lpo.mk: $(LP_FILES:%.lp=%.lpo.mk) > find . -maxdepth 1 -name '*.lpo.mk' | xargs cat...
I experimented the new `AC` on my previous test [here](https://gist.github.com/NotBad4U/1638cd3787b8e5284c7030ca8a8534ec). It is very fast now! Before we could only compute AC with ~20 variables, and I remember it took >5min...
@fblanqui I tried the new AC on my benchmarks and it is swift. I can do a computation with 500 variables, and it is faster than my current solution that...
It also does not work with my proof by reflexivity on reordering the pivot. In the code below, the algebra that represents `Clause` does not compute an AC form. The...
Thanks a lot for your work! I will give you an example as soon as possible!
Do we agree on the correctness lemmas? ``` // eval function symbol ⇓: R → ℤ; rule ⇓ (var $k $x) ↪ $k × $x with ⇓ (cst $k) ↪...
I am not sure to follow you. Do you mean putting this lemma as an axiom? `symbol f_correct : Π (r1 r2: R), π ((norm r1 =R norm r2) =...
Thanks for this exhaustive description. I think step 2) has a problem because `⇓(⇧t) ≡ t.` is incorrect because of AC. Consider the term `y + x`, which is then...
If `t` is a term of type `Z,` then I think we can easily prove that `for all t: Z, ⇓(⇧t) = t` by induction on `t.`
Maybe @fblanqui and @barras, you can add more details about this issue?