|
les entiers de PEANO revisités :
Soit le programme Prolog de définitions récursives
(inductives) des entiers naturels, des entiers pairs et des entiers impairs :
Entiers de Peano
n(0).
n(s(X)) :- n(X).
p(0).
p(s(s(X))) :- p(X).
i(s(X)) :- p(X).
|
QUESTION 1 : Construire le complété de ce
programme.
On veut prouver le séquent [ "équivalences du
Complété du Programme" ] '|-' 'A' x : (p(x) -> i(s(x)) ).
QUESTION 2 : Donnez ce séquent "en clair" et dans
la syntaxe de DJ-Prover.
QUESTION 3 : Chargez DJ-Prover sous Prolog et
Montrez la première réponse de DJ-Prover après appel de ce séquent.
On remarque que la formule à prouver est
quantifiée universellement, mais qu'il faut la prouver dans les entiers
seulement. On remarque d'autre part que la fonction "successeur" pour les
nombres pairs et impairs est s(s(x)) et NON s(x). Donc on veut faire
une preuve par induction selon le premier schéma d'induction : [F(0) , 'A' x:
(F(x) -> F(s(s(x))))] '|-' 'A' z: F(z)
QUESTION 4 : Donnez "en clair" le schéma
d'induction à proposer à DJ-Prover et montrez la réponse obtenue.
Vous devriez obtenir quelquechose du genre :
| c(1) :: A x: (p(x)->i(s(x)))
les règles applicables sont: 0 : retour arrière ,
1: intro. lemme, 2: reec. par equivalence, 3: conjecture,
4: (h(1), A|-), 5: (h(2), A|-), 6: (c(1), |-A), 7: (c(1), |-ind).
votre choix ?:7.
|
| Donnez un theoreme de la forme:
| [F(0) , 'A' x: (F(x) -> F(s(x)))] '|-' 'A' z: F(z) ou de la forme
| ['A' x: ('A' y:(y<x -> F(y)) -> F(x))] '|-' 'A' z: F(z) :
| (ci-dessus '0' et 's' tiennent lieu des constantes et symboles
fonctionnels pertinents)
| à compléter....
|
QUESTION 5 : l'équivalence pour n/1 sera-t-elle
utile dans la démonstration ?
|
|
Question 1: |
| |
Complété du
programme:
A x: n(x) <-> x=0 v (E y: x=s(y) & n(y) )
A x: p(x) <-> x=0 v (E y: x=s(s(y)) & p(y) )
A x: i(x) <-> E y: x=s(y) & p(y)
Axiomes de l'égalité:
A x: x = x
A x,y: x=y -> y=x
A x,y,z: x=y ^ y=z -> x=z
Substitution des egaux:
A x,y: ( x=y & n(x) ) -> n(y)
A x,y: ( x=y & p(x) ) -> p(y)
A x,y: ( x=y & i(x) ) -> i(y)
A x,y: ( x=y -> s(x) = s(y) )
A x: ~(s(x) = 0)
A x,y: (x != y-> s(x) != s(y) )
A x: ~(s(x) = x)
|
|
|
Question 2: |
| |
Séquent:
A x: n(x) <-> x=0 v (E y: ( x=s(y) & n(y) ) )
& A x: p(x) <-> x=0 v (E y: ( x=s(s(y)) & p(y) ) )
& A x: i(x) <-> E y: ( x=s(y) & p(y) )
|- A x: p(x) -> i(s(x))
Syntaxe DJ-Prover
['A' x : (n(x) <-> ( x=0 v 'E' y : ( x=s(y) & n(y) ))),
'A' x : (p(x) <-> ( x=0 v 'E' y : ( x=s(s(y)) & p(y) ))),
'A' x : (i(x) <-> 'E' y : ( x=s(y) & p(y) )) ]
'|-' 'A' x : (p(x) -> i(s(x)) ).
|
|
|
|
Question 3: |
| |
Réponse de
DJ-Prover au séquent.
?- ['A' x : (n(x) <-> ( x=0 v 'E' y : ( x=s(y) & n(y) ))),
'A' x : (p(x) <-> ( x=0 v 'E' y : ( x=s(s(y)) & p(y) ))),
'A' x : (i(x) <-> 'E' y : ( x=s(y) & p(y) )) ]
'|-' 'A' x : (p(x) -> i(s(x)) ).
Soit prouver :
|
| h(1) :: A x: (n(x)<->x=0 v E y: (x=s(y)&n(y)))
| h(2) :: A x: (p(x)<->x=0 v E y: (x=s(s(y))&p(y)))
| h(3) :: A x: (i(x)<->E y: (x=s(y)&p(y)))
| |-
| c(1) :: A x: (p(x)->i(s(x)))
les règles applicables sont: 0 : retour arrière ,
1: intro. lemme, 2: reec. par equivalence, 3: conjecture,
4: (h(1),A|-), 5:(h(2), A|-),6:(h(3), A|-),7:(c(1),|-A),8:(c(1),|-ind).
votre choix ?:
|
|
|
|
Question 4: |
| |
soit F(x) = p(x)
-> i(s(x))
Si on veux [F(0) , 'A' x: (F(x) -> F(s(s(x))))] '|-' 'A' z: F(z), alors:
F(0) = p(0) -> i(s(0))
F(x) = p(x) -> i(s(x))
et F(s(s(x))) = p(s(s(x))) -> i(s(s(s(x))))
Syntaxe DJ-prover:
[ p(0) -> i(s(0)) , 'A' x: ( ( p(x) -> i(s(x)) ) -> ( p(s(s(x))) ->
i(s(s(s(x)))) ) ) ]
'|-' 'A' z: (p(z)->i(s(z))).
Réponse du DJ-prover:
?- ['A' x : (n(x) <-> ( x=0 v 'E' y : ( x=s(y) & n(y) ))),
'A' x : (p(x) <-> ( x=0 v 'E' y : ( x=s(s(y)) & p(y) ))),
'A' x : (i(x) <-> 'E' y : ( x=s(y) & p(y) )) ]
'|-' 'A' x : (p(x) -> i(s(x)) ).
| | |
Soit prouver :
|
| h(1) :: A x: (n(x)<->x=0 v E y: (x=s(y)&n(y)))
| h(2) :: A x: (p(x)<->x=0 v E y: (x=s(s(y))&p(y)))
| h(3) :: A x: (i(x)<->E y: (x=s(y)&p(y)))
| |-
| c(1) :: A x: (p(x)->i(s(x)))
les règles applicables sont: 0 : retour arrière ,
1: intro. lemme, 2: reec. par equivalence, 3: conjecture,
4: (h(1), A|-),5: (h(2),A|-),6:(h(3), A|-),7:(c(1),|-A),8:(c(1),|-ind).
votre choix ?:8.
|
| Donnez un theoreme de la forme:
| [F(0) , 'A' x: (F(x) -> F(s(x)))] '|-' 'A' z: F(z) ou de la forme
| ['A' x: ('A' y:(y<x -=""> F(y)) -> F(x))] '|-' 'A' z: F(z) :
| (ci-dessus'0'et's'sont des constantes et symboles fonctionnels pertinents)
| [ p(0) ->i(s(0)) ,'A'x:(( p(x)-> i(s(x)))->(p(s(s(x)))-> i(s(s(s(x))))))]
'|-' 'A' z: (p(z)->i(s(z))).
|
|| par |-ind : en fin...
|| h(1) :: A x: (n(x)<->x=0 v E y: (x=s(y)&n(y)))
|| h(2) :: A x: (p(x)<->x=0 v E y: (x=s(s(y))&p(y)))
|| h(3) :: A x: (i(x)<->E y: (x=s(y)&p(y)))
|| h(4) :: A z: (p(z)->i(s(z)))
|| |-
|| c(1) :: A x: (p(x)->i(s(x)))
|| par |-ind : 21 (différée) et : 11
|| h(1) :: A x: (n(x)<->x=0 v E y: (x=s(y)&n(y)))
|| h(2) :: A x: (p(x)<->x=0 v E y: (x=s(s(y))&p(y)))
|| h(3) :: A x: (i(x)<->E y: (x=s(y)&p(y)))
|| |-
|| c(1)::(p(0)->i(s(0)))&A x:((p(x)->i(s(x)))->p(s(s(x)))->i(s(s(s(x)))))
les règles applicables sont: 0 : retour arrière ,
1: intro. lemme, 2: reec. par equivalence, 3: conjecture,
4: (h(1), A|-), 5: (h(2), A|-), 6: (h(3), A|-), 7: (c(1), |-&).
votre choix ?:
|
|
|
|
Question 5: |
| |
l'équivalence pour
n/1 ne sera pas utile a la démonstration, car ni p/1 ni i/1, ne font
"appel" a n/1.
|
|