Un algorithme ou mécanisme déterministe qui, pour toute formule d'un fragment ou d'une théorie logique spécifiée, termine et déclare correctement si la formule est satisfaisable (ou appartient à la théorie), en respectant des garanties de correction et d'exhaustivité pour ce fragment.

Principe

Restreindre le langage ou la théorie à un fragment décidable et concevoir des règles ou algorithmes terminants et corrects (souvent via des formes normales, constructions d'automates, clôture de congruence, élimination de quantificateurs ou tableaux) qui explorent exhaustivement l'espace de recherche dans des ressources finies.

Démonstration

Une procédure de décision pour l'égalité avec fonctions non interprétées (EUF) basée sur la clôture de congruence décide de manière déterministe si un ensemble d'égalités et de différences est satisfaisable en maintenant des classes d'équivalence et en propageant des fusions jusqu'à ce qu'une contradiction soit dérivée ou qu'un modèle soit construit.

Mauvaise application

Appliquer une procédure de décision hors de son fragment déclaré (par exemple utiliser une procédure de Presburger sur des formules avec multiplication de variables quantifiées) peut entraîner non-termination ou réponses incorrectes ; considérer un solveur incomplet comme procédure de décision peut conduire à accepter de manière non fondée des affirmations de satisfaisabilité.

Conséquence

Lorsqu'elle existe pour une théorie, une procédure de décision permet de construire des composants de raisonnement modulaires dans des systèmes plus larges (p. ex. solveurs SMT), offre des garanties automatisées de correction pour ce fragment et permet l'automatisation complète des tâches de vérification exprimables dans le fragment.

Inversion

L'inverse est une méthode indécidable ou semi-décidante qui peut ne pas terminer sur toutes les entrées ou ne renvoyer que des réponses partielles (p. ex. recherche énumérative ou solveurs heuristiques) ; ces méthodes échangent complétude et terminaison contre une applicabilité plus large.

Limite

S'applique aux algorithmes avec terminaison et correction prouvées sur un fragment logique ou une théorie clairement spécifiée. Exclut les heuristiques, approximations, procédures semi-décidantes susceptibles de diverger et méthodes ne produisant que des réponses probables ou statistiques.

Tension sémantique

Il existe une tension entre la généralité du fragment logique (les fragments plus larges sont souvent indécidables) et la tractabilité algorithmique ; une autre tension oppose la création d'une procédure complète mais coûteuse à l'utilisation de heuristiques incomplètes mais rapides en pratique.

Synthèse

Une procédure de décision est un algorithme formellement spécifié adapté à un fragment décidable qui garantit terminaison et réponses correctes oui/non sur la satisfaisabilité, atteignant cela en restreignant l'expressivité et en utilisant des techniques symboliques ou basées sur automates qui parcourent complètement l'espace de recherche du fragment.