Vérification de la Conséquence Logique

La procédure décisionnelle ou la tâche algorithmique consistant à déterminer si un ensemble de prémisses Γ implique sémantiquement une conclusion φ dans une logique et une sémantique données (noté Γ ⊨ φ), souvent par recherche de preuves ou de contre-modèles.