Herbrand-interpretáció
A Herbrand-interpretációk a matematikai logikában használatos interpretációk egy speciális családját jelentik, melyeket elsősorban a rezolúciós kalkulusban használnak fel. Ezen interpretációk elvét az adja, hogy benne minden konstansszimbólum önmagát, míg minden függvényszimbólum egy őt használó függvényt értelmez. A fontossága ezen logikai modelleknek Herbrand-tételében rejlik, mely kimondja, hogy ha egy S klóz kielégíthető bármely interpretációban, akkor S kielégíthető az ő Herbrand-interpretációjában is, és fordítva: Ha S nem elégíthető ki az ő Herbrand-interpretációjában, akkor semmilyen interpretációban sem kielégíthető.
Névadója Jacques Herbrand.
Formális definíció
szerkesztésHa egy adott S klózhalmaz leíró nyelvéhez elkészítjük az ő Herbrand-univerzumát, akkor azon interpretációt Herbrand-interpretációnak nevezzük, ahol teljesülnek a következők:
- minden konstansszimbólumhoz a Herbrand-univerzumon létező önmagát rendeli
- minden függvényszimbólumhoz azt a műveletet rendeli hozzá, amely a Herbrand-univerzumon, de azonos változókkal, azonos logikai értéket vesz fel minden esetben, vagyis:
Példa
szerkesztésLegyen . Ennek Herbrand-univerzuma ekkor: , ha bevezetjük konstanst. Ekkor S Herbrand-bázisa lesz. Ha feltételezzük, hogy -hoz kétféle interpretációt tudunk társítani, miszerint értéke akkor igaz, ha 1, vagy akkor igaz, ha 2, akkor kétféle Herbrand-interpretáció létezik az adott esetben:
- Ha a = 2, akkor:
- Ha a = 1, akkor a fentihez hasonlatosan, csak minden term ellentétesen negálva szerepel.
Források
szerkesztés- Pásztorné Varga Katalin, Várterész Magda. A matematikai logika alkalmazásszemléletű tárgyalása. Panem Kiadó, Budapest (2003). ISBN 9635453647