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) Důkaz správnosti úsudku

Logo Matematická biologie

Důkaz správnosti úsudku

Chceme-li zjistit zda klauzule je důsledkem (logickým a tedy i sémantickým) množiny klauzulí , vytvoříme množinu  a zjistíme, zda je splnitelná, či nikoliv. Je-li splnitelná ϕ není důsledkem . Je-li nesplnitelná, je důsledkem . Jinými slovy můžeme říci, že z množin předpokladů  plyne důsledek právě když množina  obsahuje prázdnou klausuli .

 

Úloha: Dokažme správnost úsudku:

Kdo zná Pavla a Marii, ten Marii lituje.             

Někteří nelitují Marii, ačkoli ji znají.               

–––––––––––––––––––––––––––––––

Někdo zná Marii, ale ne Pavla.                                            

Řešení:

     odstranění implikace (1. předpoklad)
                                    Skolemizace (2. předpoklad)
                              negovaný závěr (přejmenování )

Klausule:

  1.      
  2.    
  3.     
  4.          rezoluce 1., 2., substituce
  5.                                             rezoluce 3., 5.
  6.                                  rezoluce 4., 6., substituce
  7.                                                 rezoluce 3., 7.

Vyšla prázdná klauzule, z čehož plyne že množina je nesplnitelná (kontradikce), proto je původní úsudek logicky správný.

 

Úloha: Dokažme správnost úsudku:

Všichni členové vedení jsou majiteli obligací nebo akcionáři.
Žádný člen vedení není zároveň majitel obligací i akcionář.
Všichni majitelé obligací jsou členy vedení.
––––––––––––––––––––––––––––––––––––––––––––––––
Žádný majitel obligací není akcionář.

Řešení:

           
            

         

–––––––––––––––––––––

Klausule: 

  1.                               1. předpoklad
  2.                         2. předpoklad
  3.                                            3. předpoklad
  4.                                                             negovaný závěr
  5.                                                             (po Skolemizaci)
  6.                                          rezoluce 2., 3.
  7.                                                          rezoluce 4., 6., substituce
  8.                                                                  rezoluce 5., 7.

Úsudek je správný.

        Poznámka: Všimněme si, že jsme první klausuli při důkazu nepoužili. Tedy závěr vyplývá již z druhého a třetího předpokladu (první je pro odvození důsledku nadbytečný).

 

Úloha: Dokažme správnost úsudku:

        Každý, kdo má rád Jiřího, bude spolupracovat s Milanem.

        Milan nekamarádí s nikým, kdo kamarádí s Láďou.

        Petr bude spolupracovat pouze s kamarády Karla.

        ––––––––––––––––––––––––––––––––––––––––––––––

        Jestliže Karel kamarádí s Láďou, pak Petr nemá rád Jiřího.

Řešení:

      

      

       

        ––––––––––––––––––––

      

        Klausule:

  1.          1. předpoklad
  2.      2. předpoklad
  3.         3. předpoklad
  4.                               negovaný
  5.                                   závěr
  6.                          rezoluce 4., 2., substituce
  7.                              rezoluce 4., 2., substituce
  8.                                rezoluce 4., 2., substituce
  9.                                              rezoluce 5., 8.

Úsudek je správný.

 

Úloha: Dokažme správnost úsudku:

Každý muž má rád fotbal a pivo.

Xaver má rád pouze milovníky fotbalu a piva.

Někteří milovníci fotbalu nemají rádi pivo.

–––––––––––––––––––––––––––––––––––––

Některé ženy nemá Xaver rád.

Řešení:

                1. předpoklad

         2. předpoklad

                                  3. předpoklad

                                     negovaný závěr: ,

                                           (žena = není muž)

Kluasule:

  1.  
  2.  

  3. --------------------------------------------
  4.                                             rezoluce 4., 6.
  5.                                                       rezoluce 7., 8.
  6.                                                    rezoluce 2., 9.
  7.                                                                  rezoluce 6., 10.

Úsudek je správný.

 

 
vytvořil Institut biostatistiky a analýz Lékařské fakulty Masarykovy univerzity