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) Skolemizace

Logo Matematická biologie

Skolemizace

Máme-li formuli tvaru , podmínku na existenci y můžeme chápat jako podmínku na existenci zobrazení (tzv. výběrové funkce), která pro konkrétní hodnoty  konstruuje požadované . Místo uvažované klauzule s existenčním kvantifikátorem tak můžeme uvažovat skolemizovanou formuli . Provedeme-li tuto úpravu s každým existenčním kvantifikátorem zevně dovnitř (vždy při tom volíme nový funkční symbol pro skolemizační funkci), zbavíme se všech existenčních kvantifikátorů. Jedná-li se o funkci nulové arity (), použijeme nový konstantní symbol a, který nazýváme skolemizační konstanta.

Touto úpravou jsme neobdrželi logicky ekvivalentní formuli a interpretace funkční proměnné nebyla nijak stanovena. Půjde nám ale opět jen o splnitelnost. Pro důkaz nesplnitelnosti budeme potřebovat ukázat, že všechny instance proměnných vedou ke sporu - o interpretaci funkce se tak nemusíme zajímat, protože nebude vyhovovat žádná.

Úloha: Proveďte skolemizaci formule

Řešení

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