Határozzuk meg, hogy mely helyettesítések megengedettek a következő formula számára, majd végezzük el a szabályos helyettesítést.
Bizonyítsuk be, hogy
ha a
kifejezésben nincs
-beli változókat megnevező kvantor, akkor
megengedett
számára.
ha a
helyettesítő termekben nincs változó, akkor
megengedett minden kifejezés számára.
Határozzuk meg az alábbi termhelyettesítések kompozícióját.
Döntsük el Robinson és Herbrand algoritmusaival, hogy illeszthetők-e a következő halmazok atomi formulái egymáshoz.
Határozzuk meg, hogy amikor a Robinson-algoritmus véget ér, milyen összetettségűek lesznek a
halmaz egymáshoz illesztett atomjaiban a termek.Írjunk programot, amely Herbrand vagy Robinson algoritmusát alkalmazva megkeresi egy atomhalmaz legáltalánosabb illesztő helyettesítését.
