Examen de Logique du premier ordre

Examen de Logique du premier ordre de janvier 2001

Tous documents autorisés. Durée 2h.

Exercice 1 (4,5 points)

Montrer en calcul en calcul des séquents les énoncés suivants en ne vous servant que des règles de bases du calcul des séquents et éventuellement les règles dérivées contr, MP, abs :
Ø (PÙ Q)® (P® Ø Q)
Ø (" x(P(x)® Q(x))) |- $ x(P(x)Ù Ø Q(x))
" x(P(x)® Q(x)) |- Ø ($ x(P(x)Ù Ø Q(x)))

Exercice 2 (5 points)

On définit le prédicat Pair comme suit :
Pair(x) =_def xÎ N Ù $ n(nÎ N Ù x=2*n)
Soit SÎ seq(N)

Traduire les phrases suivantes :
1. Tous les éléments de S sont pairs.
2. Aucun élément de S n'est pair.
3. Au moins un élément de S est pair.
4. Les éléments de S référencés par des entiers pairs forment une suite décroissante.
Ecrire la spécification d'un programme qui teste si tous les éléments d'une suite sont pairs.
Ecrire la spécification d'un programme qui cherche l'indice du premier entier pair d'une suite d'entiers s'il existe et retourne -1 sinon.

Exercice 3 (4 points)

On suppose définie la fonction member qui teste l'appartenance d'un objet dans une suite. Donnons nous la fonction longueur :
longueur([])=0
longueur(cons(b,x))=s(long(x))

Définir par récurrence la fonction sansrep qui enlève les répétitions dans une suite.
Montrer par récurrence que
" x(xÎ seq(N) ® longueur(sansrep(x)) £ longueur(x)) On pourra avoir besoin des lemmes suivants que l'on supposera montrés :
(a) " x" y (x£ y ® s(x)£ s(y))
(b) " x" y (x£ y Ù x£ z ® x£ z)
(c) " x" y (x£ s(x))

Exercice 4 (6,5 points)

On veut formaliser partiellement le fonctionnement d'une crèche. On a besoin de faire référence aux enfants inscrits à la crèche, à leurs parents et aux professionnels qui travaillent auprès des enfants. Les enfants ont un professionnel référent dés leur entrée dans le lieu. Il y a d'autre part 3 sections dans la crèche : les petits, les moyens et les grands.
Voici les entités dont nous auront besoin :

4 ensembles : Peres, Meres, Professionnels, Enfants
4 relations :
mere_de reliant les enfants à leur mère : mere_de Î Enfants « Meres
pere_de reliant les enfants à leur mère : pere_de Î Enfants « Peres
référent_de reliant les enfants au professionnel qui est son référent : referent_de Î Enfants « Professionnels
section_de reliant les enfants à leur section : section_de Î Enfants {petits, moyens, grands}

Formaliser les contraintes suivantes :
1. Pour être inscrit à la crèche il ne faut pas être orphelin. En revanche on peut avoir un ou deux parents. Le père et la mère eventuels sont bien sûr uniques.
2. Les pères et mères connus ont tous au moins un enfants inscrit.
3. On ne peut être père et mère à la fois, ni nfants et parent, ni enfant et professionnel (en revanche rien n'interdit que les professionnels aient des enfants inscrits).
4. Chaque enfant est dans une section unique.
5. Chaque enfant a un prfessionnel référent unique.
6. Les professionnels peuvent être le référent de 0 ou plusieurs enfants mais ne peuvent être le référent d'enfants de sections différentes.
7. Les professionnels ne peuvent être référent de leurs enfants.
Définir les objets suivants en utilisant les entités précédentes :
1. l'ensemble prof_parent des professionnels qui ont des enfants à la crèche,
2. l'ensemble enfant_prof des enfants inscrit des professionnels.