1)
Exprimez
sin(p/3 + x) - sin(p/3 - x) en fonction de sin x.
2)
Démontrez
les égalités suivantes, pour tout réel x :
a) 2 cos (x + p/3) = cos x - Ö3 sin x
b) 2 sin (x + p/3) = sin x + Ö3 cos x
3)
Démontrez
les égalités suivantes, pour tout réel x :
a) Ö2 cos
(x - p/4) = sin x + cos x
b)
Ö2 sin (x - p/4) = sin x - cos x
4)
Développez
cos (a + b + c) en une somme
algébrique de produit et déduisez-en l'expression de cos 3a en fonction de cos a.
5)
Développez
sin (a + b + c) en une somme
algébrique de produit et déduisez-en l'expression de sin 3a en fonction de sin a.
6)
Montrer
que, pour tout réel x, sin 2x + 1 = (sin
x + cos x)²
Note
1 : Dans
notre modélisation, qui se concentre sur les manipulations syntaxiques et
calculatoires, l'énoncé "pour tout réel x" est ignoré. La solution
proposée par notre modèle reste valide car toutes les opérations de
transformation proposées sont universellement quantifiées.
Note
2 : Les
énoncés demandant de démontrer une égalité ont été dupliqués, en orientant la
résolution. La première version de l'exercice prent comme point de départ de la
résolution le membre de gauche de l'égalité. La seconde version considère le
membre de droite comme point de départ.
Note
3 : L'opérateur
a été complété, de manière spécifique par les éléments nécessaires au calcul
(valeur spécifique d'un cosinus/sinus d'une fraction du réel p ; (a + b + c) = (a + b) +
c ; …). Ces éléments de transformation
n'ont pas été rsjoutés de manière systématique, pour des raisons de performances.
La simulation, écrite en Prolog, et ralentie par de nombreux accés disques
(traces), était en effet relativement lente. Le lecteur se convaincra que
le seul effet d'une compléxification de l'opérateur est d'enrichir l'espace
de résolution. En conséquence, si une solution est accessible avec un opérateur
simplifié, elle l'est également avec un opérateur enrichi.