Frédéric Blanqui
Frédéric Blanqui
@NotBad4U https://gist.github.com/NotBad4U/1638cd3787b8e5284c7030ca8a8534ec now works with the last commits. Could you please provide me with a complete file to test the example with Clause too?
A first remark: the rule at line 39 catches everything and will probably be applied all the time. This is not what you expect I guess. It is an example...
Other remarks: - the rule line 51 is an extension of the rule line 50 to take car of contexts: you probably need similar extensions for other rules like the...
Proposal: ``` require open Stdlib.Z; constant symbol R : TYPE; symbol var : ℤ → ℤ → R; /* semantics: [var k x] = k * x note that the...
Do you really want/need to prove the correctness and completeness *inside* Lambdapi? To do that, you need to have a formalization of what Lambdapi is doing. A pen-and-paper proof *outside*...
Let's try to describe what we are trying to do: 1. We assume given two Lambdapi terms u and v of type Z, and we want to prove that they...
Right, but we have ⇓(⇧t) = t, don't we? And it is enough, no?
And do you agree with 5 and 6?
Concerning 6, following https://doi.org/10.4230/LIPIcs.FSCD.2022.24, you have that nf(t) is the normal form of the AC-canonical form of t wrt the rewrite relation -->_R^AC which consists in alternating rewriting wrt the...
Hi. I propose to close this issue as well because the initial problem is not clear at all, and the following discussion is not related actually.