Herbrand-interpretáció

A Wikipédiából, a szabad enciklopédiából

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és | forrásszöveg szerkesztése]

Ha egy adott S klózhalmaz leíró nyelvéhez elkészítjük az ő H Herbrand-univerzumát, akkor azon I_H interpretációt Herbrand-interpretációnak nevezzük, ahol teljesülnek a következők:

  • minden c \in Cnst konstansszimbólumhoz a Herbrand-univerzumon létező önmagát rendeli
  • minden f \in Fn 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:
    f^{I_H}(h_1,h_2,...,h_k)=f(h_1,h_2,...h_k)

Példa[szerkesztés | forrásszöveg szerkesztése]

Legyen S = \{ P(x),Q(y(f(y,z)) \}. Ennek Herbrand-univerzuma ekkor: H = \{ a, f(a,a), f(a, f(a,a)), f(f(a,a),a), ... \}, ha bevezetjük a \in Cnst konstanst. Ekkor S Herbrand-bázisa \{ P(a), Q(a,a), P(f(a,a)), Q(a, f(a,a), Q(f(a,a),a) ... \} lesz. Ha feltételezzük, hogy a-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: I_H=\{ \lnot P(a),Q(a,a), P(f(a,a)), \lnot Q(a, f(a,a)), ... \}
  • Ha a = 1, akkor a fentihez hasonlatosan, csak minden term ellentétesen negálva szerepel.

Források[szerkesztés | forrásszöveg szerkesztése]

  • Pásztorné Varga Katalin, Várterész Magda. A matematikai logika alkalmazásszemléletű tárgyalása. Panem Kiadó, Budapest (2003). ISBN 9635453647