-
Notifications
You must be signed in to change notification settings - Fork 0
/
new file
32 lines (18 loc) · 1.08 KB
/
new file
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
1.OCBSL
Use AC on :: + idempotence to define sets - should be easy but need to check it works in all cases
Option 2 : Use "sequential" to have negative cases. May work in some cases but lose some properties so need to check if good for us
2.Interpretation of LK into TYPE (Natural Deduction) May not have been done for similar cases.
(OL : Wait for possible CTRS features) Amelie shows Simon
Yassine lambdapi-logics Zenon LL
Monday:
Toutes les règles sauf SubstIff sont traduites dans les regles des bases (Implies, Not, Forall, Weakening, Swap?, Hypothesis, Cut, equality rules ?)
Une des régles a besoin de "prouver" une rewrite rule, (swap + enumerate) pas d'alternative?
private constructors or soundness?
Custom order in Dedukti?
Question: Que peut-on formaliser de ces règles dans La logique minimale (typed lambda calcul)
Traduire dans la deduction naturelle? Autres systemes ? (universel)
Ecrire un petit papier, draft
plus long term, LISA trad;
Ressources:
https://lipn.univ-paris13.fr/~mazza/teaching/ProofTheoryNotes.pdf
https://ncatlab.org/nlab/show/minimal+logic