Controle final correction pdf

Logique ENSIIE A - contr ole ?nal - CORRIGE ? Mardi mai - Sans documents - Sans calculatrice ni ordinateur Dur ?ee h Les exercices sont ind ?ependants Exercice Logique du premier ordre et syntaxe exo sur points Question point Quand dit-on qu ? une variable est libre dans une formule Une variable est dite libre dans une formule si elle possede au moins une occurrence libre Dans la suite de l ? exercice nous consid ?erons le langage du premier ordre L R S f a ou R et S d ?esignent deux symboles de relation respectivement unaire et binaire f d ?esigne un symbole de fonction unaire et a d ?esigne un symbole de constante Soit F la formule suivante ??x ??yR f x f y ?? ??zR x z ?? S x Question Les variables x et y sont-elles libres dans la formule F Justi ?ez votre r ?eponse en quelques mots point x est libre dans la formule car il existe deux occurrences libres les deuxieme et troisieme occurrences quand on lit la formule de gauche a droite En revanche y est une variable li ?ee car toutes ses occurrences une seule sont li ?ees Question Transformez la formule F pr ?ec ?edente de maniere a ce que variables li ?ees et variables libres ?eventuelles ne portent pas le m eme nom point On renomme les variables li ?ees qui ont aussi une occurrence libre Soit ici le x quanti ? ?e universellement On ne renomme pas les variables libres on changerait le sens de la formule ??u ??yR f u f y ?? ??zR x z ?? S x Question Donnez la formule F x t c ? est-a-dire la substitution de t ala variable x dans F quand t est le terme f z point ??x ??yR f x f y ?? ??vR f z v ?? S f z Cette substitution ne concerne que l ? occurrence libre de x Pour ?eviter la capture de la variable z dans le terme t f z par le quanti ?cateur on commence par renommer dans la formule F la variable li ?ee z en v puis on fait le remplacement D ? ou la formule ci-dessus Exercice Uni ?cation exo sur points Soit f un symbole de fonction d ? arit ?e Soit a une constante x y et z sont des variables Question CLes termes f x x y et f f y y z f y y z a sont-ils uni ?ables Si oui donnez un mgu uni ?cateur le plus g ?en ?eral si non dites pourquoi point On applique l ? algorithme d ? uni ?cation a base de regles f x x y ?? f f y y z f y y z a ? decomposition x ?? f y y z x ?? f y y z y ?? a ? elimination de y x ?? f a a z x ?? f a a z y ?? a

  • 183
  • 0
  • 0
Afficher les détails des licences
Licence et utilisation
Gratuit pour un usage personnel Attribution requise
Partager