Version imprimable
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.Citation:
Envoyé par maissa019
Salut !Citation:
Envoyé par Garulfo
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)))))
Hello...Citation:
Envoyé par maissa019
Je ne lis pas le code qui n'est pas convenablement indenté et présenté.
:tagcode:
J'ai pu résoudre mon problème...Merci qd même pr votre réponse !Citation:
Envoyé par Garulfo
à la prochaine, peut être !