Slovník | Vyhledávání | Mapa webu
 
Základy informatiky pro biologyTeoretické základy informatiky Predikátová logika Automatické dokazování v predikátové logice (obecná rezoluční metoda) Unifikace literálů

Logo Matematická biologie

Unifikace literálů

Chceme-li rezolvovat klauzule, brání nám to, že termy/argumenty nejsou stejné. Všechny proměnné jsou ale kvantifikovány všeobecným kvantifikátorem, a tudíž můžeme použít zákon konkretizace a pokusit se najít vhodnou substituci termů za proměnné tak, abychom dostali shodné „unifikované” literály. Je-li term substituovatelný za  ve formuli , pak .

 
vytvořil Institut biostatistiky a analýz Masarykovy univerzity | | zpětné odkazy | validní XHTML 1.0 Strict