Çözülüm Teorem İspatlama

User Rating:  / 0

Çözülüm teorem ispatlama, mantık teoremlerinin ispatlanması için A. Robinson tarafından geliştirilmiş bir tekniktir. Bu tekniğin esası şudur:

Eğer “veya” bağı ile bağlı P₁, ..., P_n önermelerinden bir Q önermesi dedüktif olarak çıkarılabiliyorsa, o zaman Q'nun değillemesini bu önermelere “ve” bağı ile kattığımız zaman bir çelişki elde ederiz. Sembollerle gösterecek olursak:

...çıkarımı geçerli ise,

...bir çelişkidir.

Bu yöntemin kullanılabilmesi için, P₁, ..., P_n önermelerinin, eşdeğerlik dönüşümleri kullanılarak “birleşimli normal biçim” denilen bir biçime getirilmesi gerekir. Bu biçim sadece “değil”, “ve” ve “veya” mantıksal bağlarını içerir.

Örnek 1:

                     P -> Q             ~P V Q          ~P V Q
                     P                   P               P
                     ------             ------          ~Q
                     Q                   Q              ------

Bu örnekte şartlı önermesi yerine, eşdeğeri konulmuştur ki bu, önermesinin normal biçimidir.

Örnek 2:

                    A -> B             ~A V B           ~A V B
                    B -> C             ~B V C           ~B V C
                    A                   A                A
                   --------           ---------         ~C
                    C                   C              ---------

Çözülüm teorem ispatlama yöntemi, yüklemler mantığının teorem ispatlama problemlerinde de uygulanmaktadır. Yüklemler mantığında teorem ispatı sırasında bireysel sabitlerin değişkenlerin yerine konulmasına “birleştirme” denilir.

Örnek 3:

                    P(x,y) -> Q(x)           ~P(x,y) V Q(x)          ~P(a,y) V Q(a)
                    P(a,y)                    P(a,y)                  P(a,y)
                    --------------           ---------------         ~Q(a)
                    Q(a)                      Q(a)                   ---------------