МЕТОД НА РЕЗОЛЮЦИЯТА

    Атомарните формули и техните отрицания се наричат с общото наименование литерали. Крайно множество от литерали се нарича дизюнкт. Един дизюнкт считаме верен в дадена конфигурация, ако поне един от литералите, принадлежащи на този дизюнкт, е верен във въпросната конфигурация. Ясно е, че според дадените дефиниции празното множество е дизюнкт, който не е верен в никоя конфигурация.Ако един дизюнкт не е празен, можем да образуваме дизюнкция на неговите елементи, взети в някакъв ред; тя очевидно е елементарна дизюнкция и е вярна точно в онези конфигурации, в които е верен даденият дизюнкт. Едно множество от дизюнкти се нарича изпълнимо, ако съществува конфигурация, в която са верни всички дизюнкти от това множество.

    Ако са дадени три дизюнкта, ще считаме, че третият е резолвента на първия и втория, ако трите дизюнкта имат съответно вида D₁И{Шa}, D₂И{a} и D₁ИD₂, където D₁ и D₂ са някои дизюнкти, а a е някоя атомарна формула. Образуването на резолвента на два дизюнкта се нарича резолюция. Методът на резолюцията е начин за изследване дали дадено множество от дизюнкти е изпълнимо и той се основава на следния критерий за неизпълнимост на множество от дизюнкти: едно множество от дизюнкти е неизпълнимо точно тогава, когато от дизюнкти, принадлежащи на това множество, чрез някакъв брой извършвания на резолюция може да се получи празният дизюнкт. Верността на това твърдение ще стане ясна от връзката на дизюнктите и резолюцията с елементарните секвенции и сечението.

    Ако G е крайно множество от атомарни формули, да се условим да означаваме с ШG множеството на техните отрицания. Дизюнкт, съответен на дадена елементарна секвенция G-:D, ще наричаме множеството (ШG)ИD. Очевидно е, че по този начин се получава взаимно еднозначно съответствие между множеството на елементарните секвенции и множеството на дизюнктите. При това една елементарна секвенция е вярна точно в онези конфигурации, в които е верен съответният й дизюнкт. Поради това едно множество от елементарни секвенции е изпълнимо точно тогава, когато е изпълнимо множеството на съответните им дизюнкти. Лесно се проверява, че при дефинираното взаимно еднозначно съответствие тройките елементарни секвенции, от които третата е сечение на първата и втората, преминават в тройките дизюнкти, от които третият е резолвента на първия и втория. Като вземем пред вид още критерия за неизпълнимост на множество от елементарни секвенции и обстоятелството, че на празната секвенция съответства празният дизюнкт, веднага виждаме верността на изказания по-горе критерий за неизпълнимост на множество от дизюнкти.

    С примери показахме как елементарни секвенции и сечение могат да се използват за изследване на изпълнимостта на някои множества от формули. Същите задачи ще могат разбира се да се решават и с използване на дизюнкти и резолюция (обикновено свеждането към множество от дизюнкти става чрез привеждане на формулите в конюнктивна нормална форма, а такова привеждане може да се извърши по различни начини, включително и чрез използване на законите за секвенции).

Последно изменение: 26.07.1999 г.