Entraînement — Logique et raisonnement (2/3)

Horn signifie au plus un positif. Une base est une conjonction de clauses; une clause est une disjonction. La clause vide est fausse, tandis que la base vide est vraie.

Variantes : Une réponse exacte selon les données; aucune approximation ou convention implicite supplémentaire.

Résultat {¬p(x)∨q(x)}. Énumérer les étapes ne signifie pas introduire des opérations inutiles.

• Éliminer → : ¬p(x)∨q(x).
• Examiner négations, renommage et préfixe; aucun existentiel à skolémiser.
• Omettre ∀; aucune distribution ni séparation nécessaire; une seule clause.
• Les neuf étapes sont : implications, négations, variables liées, préfixe, Skolem, universels, distribution, séparation, renommage entre clauses.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

x peut dépendre de z, quantifié avant lui, mais pas du y intérieur. La skolémisation conserve la satisfaisabilité en signature étendue, pas une équivalence ordinaire dans la signature initiale.

Variantes : Une réponse exacte selon les données; aucune approximation ou convention implicite supplémentaire.

La négation de l’existentiel devient universelle. Ni fonction de Skolem ni séparation en deux clauses n’est nécessaire.

• Nier l’antécédent donne ¬r(x)∨¬p(x,m).
• L’implication intérieure donne ¬∃z t(y,z)∨u(x,y), puis ∀z¬t(y,z).
• Préfixe ∀x∀y∀z, sans existentiel restant.
• Une clause : ¬r(x)∨¬p(x,m)∨s(x)∨¬t(y,z)∨u(x,y).

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Les deux existentiels sont indépendants. Les témoins restent les mêmes entre facteurs; les variables universelles deviennent locales aux clauses.

• Après négations : ∀x((∃y¬p(x,y))∨∃z(q(x,z)∧¬r(x,z))).
• Préfixe ∀x∃y∃z; témoins frais f(x),g(x).
• Clauses ¬p(x,f(x))∨q(x,g(x)) et ¬p(u,f(u))∨¬r(u,g(u)).
• Renommer x/u entre clauses tout en conservant les symboles f/g.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

La négation de p∨q produit ¬p∧¬q, puis la distribution produit deux clauses. Les parenthèses changent le résultat.

• Première formule : {¬p∨r, ¬q∨r}.
• Deuxième formule : {¬p∨¬q∨r}.
• ET relie les clauses de la base; OU relie les littéraux dans une clause.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Les variables sont locales. Confondre leurs noms entre clauses spécialise indûment la résolution. Les renommages et substitutions équivalents sont acceptables.

• Renommer C2 en ¬q(u,a)∨r(u,v).
• Unificateur {u↦b,y↦a}.
• Appliquer aux restes : ¬p(x)∨r(b,v).
• La réponse ¬p(b)∨r(b,a) est une instance spécialisée; x/v ne sont pas imposés.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

La substitution affecte aussi q(w), qui devient q(y). Elle ne supprime pas tous les littéraux d’un même prédicat.

• Choisir w↦y (ou l’inverse avec renommage cohérent).
• Résolvante p(x)∨r(x,y)∨q(y).
• Conserver p(x) : une résolution supprime un seul couple complémentaire.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Les clauses restent réutilisables. Une preuve directe de q puis r, suivie de la contradiction, convient aussi. Un arrêt sans progrès ne prouve pas ¬r.

• Ajouter ¬r.
• Résoudre ¬q∨r avec ¬r : ¬q.
• Résoudre ¬p∨q avec ¬q : ¬p.
• Résoudre p avec ¬p : □; conclure C⊨r.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

La quantification du but doit être déclarée avant de le nier. Un but existentiel aurait au contraire une négation universelle.

• ¬B=∃w∃t(¬q(a,w)∧¬r(b,t)).
• Introduire deux constantes fraîches k1/k2.
• Ajouter ¬q(a,k1) et ¬r(b,k2), sans variables universelles à leur place.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

La clause vide atteste la réfutation du but fermé; le littéral de réponse conserve la valeur cherchée. Un fait sans rapport peut rester inutilisé.

• But fermé : ajouter ¬parent(charles,marie), résoudre avec ¬pere(x,y)∨parent(x,y), puis avec le fait, obtenir □.
• Question : utiliser ¬parent(z,marie)∨reponse(z).
• Résoudre jusqu’à reponse(charles), qui conserve le témoin.
• Convention parent→enfant dans cette base.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Le tableau source reste accessible par le lien de matière. La tâche exige maintenant la justification de ses quinze lignes, et pas seulement le témoin et la conclusion générale. Les renommages uniformes et preuves équivalentes sont acceptés si chaque pas est justifié.

• 1. ¬v(x)∨¬a(x)∨¬e(x)∨¬h(x,y)∨¬h(etna,z)∨d(z,y) : règle générale; variables universelles implicites.
• 2. v(vesuve) : fait.
• 3. ¬a(vesuve)∨¬e(vesuve)∨¬h(vesuve,y)∨¬h(etna,z)∨d(z,y) : 1/2, θ={x↦vesuve}, résoudre sur v.
• 4. a(vesuve) : fait.
• 5. ¬e(vesuve)∨¬h(vesuve,y)∨¬h(etna,z)∨d(z,y) : 3/4, substitution vide, sur a.
• 6. ¬i(u)∨e(u) : conversion de Italie→Europe, u local.
• 7. ¬i(vesuve)∨¬h(vesuve,y)∨¬h(etna,z)∨d(z,y) : 5/6, θ={u↦vesuve}, sur e.
• 8. i(vesuve) : fait.
• 9. ¬h(vesuve,y)∨¬h(etna,z)∨d(z,y) : 7/8, substitution vide, sur i.
• 10. h(vesuve,1000) : fait.
• 11. ¬h(etna,z)∨d(z,1000) : 9/10, θ={y↦1000}, sur h(vesuve,y).
• 12. h(etna,k) : première clause de la négation déjà fournie, avec témoin frais k.
• 13. d(k,1000) : 11/12, θ={z↦k}, sur h(etna,z).
• 14. ¬d(k,1000) : seconde clause de cette même négation, même k.
• 15. □ : 13/14, substitution vide, sur d(k,1000).
• La négation ∃t(h(etna,t)∧¬d(t,1000)) n’est pas niée une seconde fois. Conclusion C⊨∀t(h(etna,t)→d(t,1000)); l’existence d’une hauteur dans C n’est pas prouvée séparément.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Chaque fait, règle convertie et résolvante possède une justification explicite. z↦w conserve directement le résultat ¬heureux(w); l’inverse convient seulement avec les renommages et substitutions cohérents.

• 1. ¬vie_interessante(z) : négation de ∃z vie_interessante(z), universel implicite.
• 2. ¬lire(y)∨intelligent(y) : conversion de E2.
• 3. lire(arthur) : première clause de E3, conjonction séparée.
• 4. ¬heureux(w)∨vie_interessante(w) : conversion de E4.
• 5. ¬riche(x)∨¬intelligent(x)∨heureux(x) : conversion de E1.
• 6. riche(arthur) : seconde clause de E3.
• 7. ¬heureux(w) : 1/4, θ={z↦w}, sur vie_interessante. L’orientation inverse exige un renommage cohérent du résultat.
• 8. ¬riche(w)∨¬intelligent(w) : 5/7, θ={x↦w}, sur heureux.
• 9. ¬lire(w)∨¬riche(w) : 2/8, θ={y↦w}, sur intelligent; l’ordre des littéraux ne change pas la clause.
• 10. ¬riche(arthur) : 3/9, θ={w↦arthur}, sur lire.
• 11. □ : 6/10, substitution vide, sur riche(arthur).
• C⊨∃z vie_interessante(z), témoin Arthur; pas de négation d’un simple atome libre à la place du but existentiel.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Le programme exprime les connaissances. La requête demande leur preuve; elle ne recopie pas la négation ajoutée dans la preuve sur papier.

• p(X,Y) :- q(X,Y), r(X,Y).
• Tête p à gauche, conditions q/r à droite; virgule = ET.
• Clause ¬q(x,y)∨¬r(x,y)∨p(x,y), un seul positif.
• Variables majuscules et point final; un fait est une clause positive unitaire.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

X=a serait compatible isolément, mais les seconds arguments sont incompatibles. Un atome minuscule y diffère d’une variable Y; un tiret non cité peut être un opérateur.

Variantes : Une réponse exacte selon les données; aucune approximation ou convention implicite supplémentaire.

La recherche présentée est en profondeur. Le retour arrière défait les liaisons de la branche abandonnée; une branche infinie pourrait empêcher d’autres réponses.

• Premier choix p(a,1) : X=a,Y=1; q(a,1) échoue.
• Retour arrière : abandonner ces liaisons; choisir p(b,2).
• q(b,2) réussit; réponse X=b,Y=2.
• Les variables partagées se propagent; false d’une branche n’arrête pas tous les choix.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

La petite console du support est erronée. Le lapsus X/Z de la fratrie doit aussi être lu selon les arguments de la règle.

• Réponses W=anne puis W=jimmy, pas Julie.
• Dans la grande base, la même question demanderait les enfants de Nathalie.
• Ne jamais fusionner les bases sans inverser explicitement la relation.
• parent/2 ne code pas le sexe; le nom du prédicat seul ne fixe pas le sens.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Le programme contient faits/règles et le but se termine par un point. Stop interrompt la recherche; aucune installation, création de compte ou exécution externe n’est attestée par cette révision.

Variantes : Une réponse exacte selon les données; aucune approximation ou convention implicite supplémentaire.

Exclusion de soi et unicité des réponses sont distinctes. Le placement du test suppose ici des personnes déjà instanciées.

• Anne et Jimmy sont deux parents communs : deux preuves pour chaque valeur.
• L’identité permet Nathalie dans la règle initiale.
• Le test final retire Nathalie : julie,luc,julie,luc; il ne déduplique pas.
• Au début sur X/Z libres, X=Z réussit, donc not échoue.
• Négation par échec, ni négation classique ni contrainte abstraite de différence.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Les structures et répétitions imposent les liaisons. Renommer des variables de façon uniforme est admis; transformer y minuscule en variable ne l’est pas.

• 1 : X=p(12,abc), Y=12, Z=abc.
• 2 : X=a, Z=g(h(y)); y est un atome.
• 3 : échec a/b.
• 4 : R=f(X,g(h(y))); X reste libre.
• Appliquer chaque substitution à toutes les occurrences de la variable.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

La variable partagée réalise une jointure logique. L’ordre annoncé suit celui des faits; seules ces six données sont nécessaires à cet exemple.

• parcelle(N,roland), culture(N,L), surface(N,S).
• Réponses N=2,L=carottes,S=8 puis N=6,L=pommes_de_terre,S=12.
• Le même N relie propriétaire, culture et surface; des variables indépendantes produiraient un produit cartésien erroné.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

L’ordre des sous-buts et les substitutions expliquent pourquoi c(1,1) et c(5,5) ne deviennent pas des réponses alternatives.

• a(R,T) devient b(R),c(R,R),d(T).
• b(R) devient f(R); f(3) fixe R=3 partout.
• c(3,3) réussit; d(T) fixe T=2.
• Réponse R=3,T=2; les faits e sont inutilisés.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Les cinq questions historiques sont désormais demandées sur les 24 faits, avec résultats, liaisons et limites du modèle. La matière de référence contient le programme complet; les deux bases parent/2 restent séparées.

• parent(marie,elizabeth). réussit. Le sexe n’est pas encodé; la requête seule prouve le lien parental, pas une propriété mere/2.
• parent(nathalie,X). échoue : aucun enfant décrit dans cette base; aucune vérité universelle sur sa vie réelle n’en découle.
• parent(X,patricia). donne X=robert puis X=elizabeth dans l’ordre des faits.
• parent(martin,X),parent(X,Y). donne X=kevin,Y=tom; la branche X=marc n’a pas de descendant dans cette base.
• parent(robert,X),parent(X,Y),parent(Y,sylvie). donne X=anne,Y=luc, chaîne Robert→Anne→Luc→Sylvie.
• Ne pas inverser les arguments en recopiant la petite base enfant→parent. Les variables intermédiaires sont partagées entre les sous-buts.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Les variables intermédiaires doivent être communes aux bonnes relations. Les noms de variables et une permutation sûre des buts sont acceptés si la sémantique et l’instanciation sont préservées.

• soeur_frere(X,Y):-parent(P,X),parent(P,Y),not(X=Y).
• tante_oncle(X,Y):-parent(GP,X),parent(GP,P1),not(P1=X),parent(P1,Y).
• petit_enfant(X,Y):-parent(P,X),parent(Y,P). X est petit-enfant de Y.
• cousin_cousine(X,Y):-parent(GP,P1),parent(GP,P2),not(P1=P2),parent(P1,X),parent(P2,Y).
• Les not viennent après instanciation; un parent commun suffit; des preuves répétées restent possibles.

Variantes : Autoévaluation explicite : accepter preuves, noms de variables, substitutions et formulations équivalentes si les étapes et hypothèses restent cohérentes.

Correction des règles, complétude pour réfutation, équité de la recherche et terminaison sont quatre propriétés distinctes. Ne pas conclure ¬B d’un arrêt pratique sans progrès.

Variantes : Une réponse exacte selon les données; aucune approximation ou convention implicite supplémentaire.

Un atome est un prédicat appliqué à des termes; un littéral est un atome ou sa négation. Une clause est une disjonction, et une base les relie par ET. p(a)∨q(a) a deux positifs et n’est pas Horn.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

Unitaire = un littéral; Horn = au plus un positif, donc p(a) et ¬p(a) sont Horn. Une disjonction vide est fausse; une conjonction vide est vraie. Ne pas confondre {□} avec {}.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

La majuscule initiale marque la variable. Le nom minuscule avec underscore est ici un atome; aime possède deux arguments. Un nom avec tiret non cité peut être analysé comme un opérateur.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

v dépend des universels antérieurs u; z peut dépendre de u et w. Les existentiels précédents sont déjà remplacés; g n’a pas à recevoir z lui-même comme argument. Skolem préserve la satisfaisabilité dans la signature étendue.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

Nier p∧q donne ¬p∨¬q, donc une seule clause. Le deuxième choix correspond à (p∨q)→r, plus fort; le troisième est la négation de la formule, pas sa conversion.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

Unifier q(x)/q(y) identifie leurs variables puis applique la substitution aux restes. Une constante a spécialiserait sans nécessité. Les restes sont disjoints, pas conjoints.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

Les noms de prédicat sont minuscules, les faits et règles finissent par un point, et la conséquence est en tête. La troisième proposition inverse la règle et omet le fait demandé.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

Le même N réalise la jointure. Des variables N et M séparées produiraient les quatre combinaisons. Next cherche d’autres preuves après le premier succès.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

lien instancie Y à b puis c, tous deux distincts de a; l’unification a=b ou a=c échoue, donc not réussit. Placé avant lien avec Y libre, not(a=Y) échouerait.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

La première donne petit_enfant(cy,ada). La seconde encode X grand-parent de Y, orientation inverse. La troisième partage un parent et encode une fratrie sans exclusion de soi.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

La contradiction provient de l’ajout de ¬B à C : tous les modèles de C satisfont B. Correction de cette preuve, complétude d’un calcul et terminaison d’une stratégie restent distinctes.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

Une variable répétée doit recevoir la même valeur partout. Des variables différentes peuvent recevoir a et b. Enfin t/1 et t/2 sont des structures incompatibles.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

Le corps est une conjonction et partage X. L’échec de la seconde condition annule la liaison rouge et réessaie le choix candidat. Le test d’une condition seule ne suffit pas.

Variantes : Une réponse exacte sous les conventions de l’énoncé.

Les mêmes connaissances passent des prédicats aux clauses puis au programme. La négation du but est ajoutée pour la preuve papier; le programme Prolog conserve les connaissances positives et reçoit le but en requête.

• C={capteur(c1),actif(c1),¬capteur(x)∨¬actif(x)∨alarme(x)}; ajouter ¬alarme(c1).
• Résoudre la règle avec ¬alarme(c1), θ={x↦c1} : ¬capteur(c1)∨¬actif(c1). Puis avec capteur(c1) : ¬actif(c1). Puis actif(c1) : □.
• Programme : capteur(c1). actif(c1). alarme(X):-capteur(X),actif(X). Requête : alarme(c1).
• Clauses de Horn; le fait est une clause positive unitaire, la règle a un positif; la réfutation établit C⊨alarme(c1).
• La preuve suppose les faits/règle; elle ne valide pas le capteur réel ni une garantie de terminaison pour tout programme du premier ordre.

Variantes : Les renommages uniformes et les démarches équivalentes justifiées sont acceptés.

Les règles appliquent les notions à une autre base de taille contrôlable. Vérifier aussi tante_oncle(bea,eli) et cousin(eli,cy) pour contrôler la symétrie attendue du cousinage, sans inverser les relations orientées.

• tante_oncle(X,Y):-parent(G,X),parent(G,P),not(X=P),parent(P,Y).
• cousin(X,Y):-parent(G,P),parent(G,Q),not(P=Q),parent(P,X),parent(Q,Y).
• tante_oncle(X,cy) donne X=dan; cousin(cy,Y) donne Y=eli. Un seul parent commun dans cette base, donc une preuve par réponse.
• Les tests viennent après les faits liant leurs arguments. parent/2 n’établit pas le sexe; parent→enfant ne se fusionne pas avec enfant→parent.

Variantes : Les renommages uniformes et les démarches équivalentes justifiées sont acceptés.