Herbrand-tétel

Kapcsolódó fogalmak: 
Herbrand-univerzum
Kapcsolódó fogalmak: 
Herbrand-bázis
Rövid szöveges bemutatás: 
A Herbrand-tétel a logikai állítások cáfolásával foglalkozik. A tétel kimondása előtt, úgy döntötték el egy állítás cáfolhatóságát, hogy az állítás minden interpretációját megvizsgálták, és ha egyikben sem volt kielégíthető akkor valóban nem volt kielégíthető. Ehhez képest a Herbrand tétel azt mondja ki, hogy egy állítás cáfolhatóságához elegendő, csak a Herbrand univerzumban létező minden interpretáció cáfolhatóságát vizsgálni, ami jóval kisebb feladatot jelent. Tehát egy klóz akkor kielégíthetetlen, ha összes Herbrand interpretációja a Herbrand univerzumban kielégíthetetlen.