5 Mars 2025
Dans tout cet exercice, F est une formule sous forme normale conjonctive et on note res(C,D) le resolvant de deux clauses.
1.a. Vrai : si τ est un modèle de F, alors il satisfait toutes les clauses de F. En particulier, il satisfait toutes les clauses de F \ {C}. Donc F \ {C} est satisfiable.
1.b. Vrai, res(C,D) est une conséquence logique de F donc si τ ⊨ F, τ ⊨ res(C,D). A fortiori, τ ⊨ F ∧ res(C,D). Donc si F est satisfiable, F ∧ res(C,D) l’est aussi.
1.c. Faux : toutes les formules contradictoire ont une réfutation en résolution, c’est la complétude de la résolution. On l’a prouvé en cours en utilisant la résolution de Davis-Putnam.
Pour chacune des formules suivantes, écrire l’arbre syntaxique et donnez les variables libres.
Formalisez en logique du premier ordre les énoncés ci-dessous dans le langage du premier ordre n’ayant pas de constante, pas de symbole de constantes et les prédicats suivant (l’arité est donnée entre parenthèse) : Grenouille(1), Mouche(1), Amphibiens(1), Insecte(1), Animal(1), AimeManger(2). Pour chacune des formules que vous avez écrites, donnez un modèle et un contre-modèle.
Un modèle : on considère l’univers U = {G, M}, Grenouille = Amphibien = {G} et Mouche = Insecte = {M}. Remarquons que si on prend Grenouille = Mouche = ∅, ça marche aussi!
Pour un contre modèle, toujours sur l’univers U = {G, M}, on prend Grenouille = {G}, Amphibien = ∅ (et ce qu’on veut pour Mouche et Insecte).
Un modèle : toujours sur l’univers U = {G, M}, Grenouille = {G} et Mouche = {M} et AimeManger = {(G,M)}.
Un contre-modèle : Grenouille = {G} et Mouche = {M} et AimeManger = ∅.
Un modèle : sur l’univers U = {A}, Animal = {A} et Mouche = Grenouille = ∅.
Un contre-modèle : sur l’univers U = {A}, Animal = Grenouille = {A}.
Un modèle : Animal = {A}, Grenouille = {A}, Mouche = ∅.
Un contre-modèle : Animal = {A}, Grenouille = {A}, Mouche = {A}.
Donnez les formules obtenues après avoir appliqué les substitutions demandées.
∃u(R(u,g(x,x))∧∃y.S(y)).