Entscheidungsverfahren

Ein deterministischer Algorithmus oder Mechanismus, der für jede Eingabeformel in einer bestimmten logischen Theorie oder einem Fragment terminiert und korrekt entscheidet, ob die Formel erfüllbar ist (oder zur Theorie gehört), gemäß Soundness- und Vollständigkeitsgarantien für dieses Fragment.