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
Sémantique opérationnelle
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.
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 .
Nous sommes alors dans la théorie des modèles, lorsque nous écrivons , nous devons être capable de prouver par table de vérité toutes les combinaisons. Nous sommes en présence de tautologies.
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 , 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
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 et de l'affirmation de implique , qui nous permet de déduire .
La formule du modus ponens est donc : .
Modus tollens
La règle du modus tollens est la contraposition que nous avons vu lors de l'algèbre booléen. Si n'est pas vrai et que implique , alors nous pouvons déduire que n'est pas vrai non plus.
La formule du modus tollens est donc :
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 :
Complétude et cohérence
Soit notre ensemble des propositions , notre système est complet ssi . Cela revient à dire que le système est complet si nous pouvons démontrer toutes les tautologies.
Notre système est cohérent5 ssi . Cela revient à dire que tous les théorèmes sont alors des tautologies.
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é.
Deutsche Übersetzung
Sie haben gebeten, diese Seite auf Deutsch zu besuchen. Momentan ist nur die Oberfläche übersetzt, aber noch nicht der gesamte Inhalt.Wenn Sie mir bei Übersetzungen helfen wollen, ist Ihr Beitrag willkommen. Alles, was Sie tun müssen, ist, sich auf der Website zu registrieren und mir eine Nachricht zu schicken, in der Sie gebeten werden, Sie der Gruppe der Übersetzer hinzuzufügen, die Ihnen die Möglichkeit gibt, die gewünschten Seiten zu übersetzen. Ein Link am Ende jeder übersetzten Seite zeigt an, dass Sie der Übersetzer sind und einen Link zu Ihrem Profil haben.
Vielen Dank im Voraus.
Dokument erstellt 15/06/2010, zuletzt geändert 28/10/2018
Quelle des gedruckten Dokuments:https://www.gaudry.be/de/programmation-declarative-operationnelle-rf-mathml.html
Die Infobro ist eine persönliche Seite, deren Inhalt in meiner alleinigen Verantwortung liegt. Der Text ist unter der CreativeCommons-Lizenz (BY-NC-SA) verfügbar. Weitere Informationen auf die Nutzungsbedingungen und dem Autor.
- ↑ 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.
- ↑ 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.
Referenzen
IHDCB337 - Technique d'intelligence artificielle : JM Jacquet, Programmation déclarative
(2009)- IHDCB337 - Technique d'intelligence artificielle : H Toussaint,
Tp
(2009)
Diese Verweise und Links verweisen auf Dokumente, die während des Schreibens dieser Seite konsultiert wurden, oder die zusätzliche Informationen liefern können, aber die Autoren dieser Quellen können nicht für den Inhalt dieser Seite verantwortlich gemacht werden.
Der Autor Diese Website ist allein dafür verantwortlich, wie die verschiedenen Konzepte und Freiheiten, die mit den Nachschlagewerken gemacht werden, hier dargestellt werden. Denken Sie daran, dass Sie mehrere Quellinformationen austauschen müssen, um das Risiko von Fehlern zu reduzieren.
