Style des formules

Les formules sont affichées en MathML, ces fonctions d'affichage sont en test et ne sont pas garanties.
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

No cache version.

Caching disabled. Default setting for this page:enabled (code LNG204)
If the display is too slow, you can disable the user mode to view the cached version.

Sémantique opérationnelle

Contents

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énotationnelle¹, et la sémantique opérationnelle.

Contents Haut

Satisfaction, conséquence logique

Nous pouvons dire qu'un ensemble de formules {f₁,...,f_n} 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 $⊨$ .

Nous sommes alors dans la théorie des modèles, lorsque nous écrivons $⊨ p ∧ q ⇒ q$ , nous devons être capable de prouver par table de vérité toutes les combinaisons. Nous sommes en présence de tautologies.

Contents Haut

Déduction

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

Nous sommes alors dans la théorie de la démonstration, lorsque nous écrivons $⊢ p ∧ q ⇒ 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 ⇒ (Q ⇒ P)$
$(P ⇒ (Q ⇒ R)) ⇒ ((P ⇒ Q) ⇒ (P ⇒ R))$
$(¬ Q ⇒ ¬ P) ⇒ (P ⇒ 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émisse² 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 conjonction³ 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 ⇒ Q ⊢ Q$ .

Contents 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 : $¬ Q, P ⇒ Q ⊢ ¬ P$

Contents 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 ⇒ Q, Q ⇒ R ⊢ P ⇒ R$

Contents Haut

Complétude et cohérence

Soit notre ensemble des propositions $S$ , notre système est complet ssi $S ⊨ P ⇒ S ⊢ P$ . Cela revient à dire que le système est complet si nous pouvons démontrer toutes les tautologies.

Notre système est cohérent⁵ ssi $S ⊢ P ⇒ S ⊨ P$ . Cela revient à dire que tous les théorèmes sont alors des tautologies.

Contents 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é.

Contents 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

English translation

You have asked to visit this site in English. For now, only the interface is translated, but not all the content yet.

If you want to help me in translations, your contribution is welcome. All you need to do is register on the site, and send me a message asking me to add you to the group of translators, which will give you the opportunity to translate the pages you want. A link at the bottom of each translated page indicates that you are the translator, and has a link to your profile.

Thank you in advance.

Document created the 15/06/2010, last modified the 28/10/2018
Source of the printed document:https://www.gaudry.be/en/programmation-declarative-operationnelle-rf-mathml.html

The infobrol is a personal site whose content is my sole responsibility. The text is available under CreativeCommons license (BY-NC-SA). More info on the terms of use and the author.

Notes

↑ sémantique dénotationnelle : sémantique du point fixe, en utilisant un opérateur de transformation des interprétations de Herbrand.
↑ Premisse : Ce sont les différentes formules nécessaires à la dérivation (la déduction) de la conclusion.
↑ Conjonction : En raisonnement logique, des affirmations séparées par une virgule sont liées par l'opérateur ET, qui est la conjonction.
↑^a,b ssi : si et seulement si
↑ 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.

Contents Haut

References

IHDCB337 - Technique d'intelligence artificielle : JM Jacquet, Programmation déclarative (2009)
IHDCB337 - Technique d'intelligence artificielle : H Toussaint, Tp (2009)

These references and links indicate documents consulted during the writing of this page, or which may provide additional information, but the authors of these sources can not be held responsible for the content of this page.
The author This site is solely responsible for the way in which the various concepts, and the freedoms that are taken with the reference works, are presented here. Remember that you must cross multiple source information to reduce the risk of errors.

Contents Haut

Sémantique opérationnelle

Satisfaction, conséquence logique