Discussion :

[maissa019]

Salut,

ACL2, A Computationnal Logic for Applicative Common Lisp, est un démonstrateur de théorèmes semi-automatique utilisant le langage Common Lisp. Alors, je voudrais savoir s'il y a par hasard sur ce forum des personnes qui ont une connaissance de cet outil ???

Merci

[Garulfo]

Salut,

ACL2, A Computationnal Logic for Applicative Common Lisp, est un démonstrateur de théorèmes semi-automatique utilisant le langage Common Lisp. Alors, je voudrais savoir s'il y a par hasard sur ce forum des personnes qui ont une connaissance de cet outil ???

Merci

Disons que oui.

[maissa019]

Disons que oui.

Salut !

Alors voilà, j'ai le problème suivant. Je viens de définir en Common Lisp:
-une fct convert-y qui sert à convertir un nb binaire (représenté par une liste) en sa représentation décimale,
-un prédicat valid-01 qui permet de reconnaitre une liste qui n'est formée que de 0 et de 1.
-le théorème convert-y-<-expt qui dit que si on a une liste valide de 0 et de 1 alors le résultat de la conversion de cette liste par la fct convert-y, serait inférieur à (expt 2 (len y)).
convert-y
Exple: '(1 0 0)---------------> 4 < (expt 2 3)=8

Alors mon problème est d'arriver à démontrer dans ACL2 ce théorème ? est ce que vous pourriez m'aider en me donnant des indications ?

Ci-dessous, le code Common Lisp de mes fcts:

(defun convert-y (y)
(if (endp y) 0
(let* ((e (len (cdr y)))
(a (expt 2 e)))
(+ (* (car y) a) (convert-y (cdr y))))))
;(if (or (equal (car y) 0) (equal (car y) 1))
;;
(defun valid-01 (y)
(if (endp y) t
(and (or (equal (car y) 0) (equal (car y) 1)) (valid-01 (cdr y)))))
;;
(defthm convert-y-<-expt
(implies (valid-01 y)
(< (convert-y y) (expt 2 (len y)))))

[Garulfo]

Salut ![...]

Hello...

Je ne lis pas le code qui n'est pas convenablement indenté et présenté.

[maissa019]

Hello...

Je ne lis pas le code qui n'est pas convenablement indenté et présenté.

J'ai pu résoudre mon problème...Merci qd même pr votre réponse !
à la prochaine, peut être !