Procédure de Décision

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.