Matematické Fórum

Ahoj,
řeším v predikátové logice úlohu, kdy mám teorii zapsanou v CNF a formuli , kterou lze v zamítnout pomocí rezoluce.

Otázka zní, zda ji lze zamítnout pomocí LI-rezoluce. Ta je (nepletu-li se) definována tak, že i musejí být Hornovy formule, tedy musí sestávat z Hornových klauzulí (tedy každá klauzule může obsahovat nejvýše jeden pozitivní literál).

Abych ukázal dokazatelnost pomocí LI-rezoluce, stačí i převést do tvaru Hornovy formule.

Nevím ale, zda lze nějak jednoduše převést klauzuli obsahující více pozitivních literálů na jednu či více Hornových klauzulí. Jde to? Já myslím, že ne, ale nenapadá mě, jak to jednoduše ukázat.

Pro příklad řekněme, že mám všechny klauzule v CNF Hornovské, až na tuto následující: . Lze ji nějak převést na Hornovské klauzule?

Předem díky...