Style des formules

Les formules sont affichées en texte
Cette page utilise des fonctions particulières d'affichage de formules (plus d'infos) , vous pouvez choisir entre un affichage mathml, un affichage html, et un affichage texte

Geen cache-versie.

Caching uitgeschakeld. Standaardinstelling voor deze pagina:ingeschakeld (code LNG204)
Als het scherm te langzaam is, kunt u de gebruikersmodus uitschakelen om de cacheversie te bekijken.

Sémantique opérationnelle

Inhoudsopgave

Jusqu'à présent, nous nous sommes occupés de la sémantique déclarative lorsque nous avons envisagé la programmation logique,mais il existe aussi la sémantique dénotationnelle1, et la sémantique opérationnelle.

Inhoudsopgave Haut

Satisfaction, conséquence logique

Nous pouvons dire qu'un ensemble de formules {f1,...,fn} satisfait une formule f si, pour toute interprétation et pour toute formule de l'ensemble, nous avons « vrai ».

En sémantique déclarative, la conséquence logique se note (  CONSEQUENCE LOGIQUE de  ) .

Nous sommes alors dans la théorie des modèles, lorsque nous écrivons (  CONSEQUENCE LOGIQUE de   ( (p ET q)  IMPLIQUE q) ) , nous devons être capable de prouver par table de vérité toutes les combinaisons. Nous sommes en présence de tautologies.

Inhoudsopgave Haut

Déduction

En sémantique opérationnelle (ou sémantique procédurale), la déduction se note (  DEDUIT  ) .

Nous sommes alors dans la théorie de la démonstration, lorsque nous écrivons (  DEDUIT   ( (p ET q)  IMPLIQUE q) ) , nous ne sommes plus obligés d'instancier toutes les variables. Nous avons à notre disposition différents « outils » tels que les axiomes de Hilbert (purement mathématique), ou les systèmes de Wang et le principe de Robinson-Herbrand (application de formules). Nous sommes en présence de théorèmes.

Le différents théorèmes que nous utiliserons le plus sont les axiomes de Hilbert et les règles d'inférence ou de dérivation.

Axiomes de Hilbert

  • (P IMPLIQUE  (  (Q IMPLIQUE P)  ) )
  • ( (  (P IMPLIQUE  (  (Q IMPLIQUE R)  ) )  )  IMPLIQUE  (  ( (  (P IMPLIQUE Q)  )  IMPLIQUE  (  (P IMPLIQUE R)  ) )  ) )
  • ( (  ( NOT (Q)  IMPLIQUE  NOT (P) )  )  IMPLIQUE  (  (P IMPLIQUE Q)  ) )

Méta règles d'inférence

En général, nous trouverons les règles d'inférence sous la forme d'une pile de prémisse2 sous laquelle nous avons un trait (comme dans nos bons vieux calculs écrits), en dessous duquel nous pouvons lire la conclusion. Comme je n'ai pas des masses de temps pour l'instant, je les représenterais sous la forme de formules (les prémisses séparés par des virgules, desquels se déduit la conclusion), et je tenterais par la suite d'ajouter une représentation plus traditionnelle.

Modus ponens

La règle du modus ponens est la conjonction3 de l'affirmation de P et de l'affirmation de P implique Q, qui nous permet de déduire Q.
La formule du modus ponens est donc : (P, (P IMPLIQUE Q)   DEDUIT  Q) .

Inhoudsopgave Haut

Modus tollens

La règle du modus tollens est la contraposition que nous avons vu lors de l'algèbre booléen. Si Q n'est pas vrai et que P implique Q, alors nous pouvons déduire que P n'est pas vrai non plus.
La formule du modus tollens est donc : ( NOT (Q) , (P IMPLIQUE Q)   DEDUIT   NOT (P) )

Inhoudsopgave Haut

Syllogisme

La règle du syllogisme (ou du chaînage) est une facilité, mais n'est pas une nécessité car elle peut se déduire d'autres règles.
La règle du syllogisme est la suivante : ( (P IMPLIQUE Q) , (Q IMPLIQUE R)   DEDUIT   (P IMPLIQUE R) )

Inhoudsopgave Haut

Complétude et cohérence

Soit notre ensemble des propositions S, notre système est complet ssi ( (S  CONSEQUENCE LOGIQUE de  P)  IMPLIQUE  (S  DEDUIT  P) ) . Cela revient à dire que le système est complet si nous pouvons démontrer toutes les tautologies.

Notre système est cohérent5 ssi ( (S  DEDUIT  P)  IMPLIQUE  (S  CONSEQUENCE LOGIQUE de  P) ) . Cela revient à dire que tous les théorèmes sont alors des tautologies.

Inhoudsopgave Haut

Décidabilité

S'il existe un algorithme permettant de déterminer en un nombre fini d'étapes si une formule est une conséquence logique, nous pouvons dire que le système est décidable.

Dans le cas de la logique déclarative, le calcul des propositions est décidable par la génération des tables de vérités. Ce n'est pas le cas pour le calcul des prédicats.

Nous utiliserons l'algorithme de Wang dans le cas de la décidabilité.

Inhoudsopgave Haut

Cette page utilise des fonctions particulières d'affichage de formules (plus d'infos) , vous pouvez choisir entre un affichage mathml, un affichage html, et un affichage texte

Nederlandse vertaling

U hebt gevraagd om deze site in het Nederlands te bezoeken. Voor nu wordt alleen de interface vertaald, maar nog niet alle inhoud.

Als je me wilt helpen met vertalingen, is je bijdrage welkom. Het enige dat u hoeft te doen, is u op de site registreren en mij een bericht sturen waarin u wordt gevraagd om u toe te voegen aan de groep vertalers, zodat u de gewenste pagina's kunt vertalen. Een link onderaan elke vertaalde pagina geeft aan dat u de vertaler bent en heeft een link naar uw profiel.

Bij voorbaat dank.

Document heeft de 15/06/2010 gemaakt, de laatste keer de 28/10/2018 gewijzigd
Bron van het afgedrukte document:https://www.gaudry.be/nl/programmation-declarative-operationnelle-rf-texte.html

De infobrol is een persoonlijke site waarvan de inhoud uitsluitend mijn verantwoordelijkheid is. De tekst is beschikbaar onder CreativeCommons-licentie (BY-NC-SA). Meer info op de gebruiksvoorwaarden en de auteur.

Notes

  1. ↑ sémantique dénotationnelle : sémantique du point fixe, en utilisant un opérateur de transformation des interprétations de Herbrand.

  2. ↑ Premisse : Ce sont les différentes formules nécessaires à la dérivation (la déduction) de la conclusion.

  3. ↑ Conjonction : En raisonnement logique, des affirmations séparées par une virgule sont liées par l'opérateur ET, qui est la conjonction.

  4. ↑a,b ssi : si et seulement si

  5. ↑ Cohérent : Nous retrouvons souvent le terme « correct », et l'on parle alors de correction au lieu de cohérence, mais si les termes ont des nuances sémantiques, le but est ici identique.

Inhoudsopgave Haut

Referenties

  1. boek Taal van het document:fr IHDCB337 - Technique d'intelligence artificielle : JM Jacquet, Programmation déclarative (2009)
  2. boek Taal van het document:fr IHDCB337 - Technique d'intelligence artificielle : H Toussaint, Tp (2009)

Deze verwijzingen en links verwijzen naar documenten die geraadpleegd zijn tijdens het schrijven van deze pagina, of die aanvullende informatie kunnen geven, maar de auteurs van deze bronnen kunnen niet verantwoordelijk worden gehouden voor de inhoud van deze pagina.
De auteur Deze site is als enige verantwoordelijk voor de manier waarop de verschillende concepten, en de vrijheden die met de referentiewerken worden genomen, hier worden gepresenteerd. Vergeet niet dat u meerdere broninformatie moet doorgeven om het risico op fouten te verkleinen.

Inhoudsopgave Haut