Çözünürlük (mantık) - Resolution (logic)

Gelen matematiksel mantık ve otomatik Teorem ispatı , çözünürlük bir olan Çıkarım kural bir yol çürütülmesi komple teoremi-kanıtlayan cümlelerin için tekniğine önermeler mantığı ve birinci dereceden mantık . Önerme mantığı için, çözümleme kuralının sistematik olarak uygulanması, Boolean tatmin edilebilirlik problemini (tamamlayıcısı) çözerek, formülün karşılanamaması için bir karar prosedürü görevi görür . İçin birinci derece mantık , çözünürlük için temel olarak kullanılabilecek yarı algoritma ve unsatisfiability sorun için birinci derece mantık aşağıdaki olandan daha pratik bir yöntem sağlamak, Gödel'in tamlık teoremi .

Çözünürlük kuralı Davis ve Putnam'a (1960) kadar götürülebilir ; ancak, algoritmaları verilen formülün tüm temel örneklerini denemeyi gerektiriyordu . Bu birleşimsel patlama kaynağı 1965'te John Alan Robinson'ın sözdizimsel birleştirme algoritması tarafından ortadan kaldırıldı , bu da ispat sırasında formülün ispat sırasında çürütmenin eksiksizliğini korumak için gerektiği kadar "talep üzerine" somutlaştırılmasına izin verdi .

Bir çözüm kuralı tarafından üretilen maddeye bazen çözücü denir .

Önerme mantığında çözüm

Çözünürlük kuralı

Çözünürlük kuralı önermeler mantığında iki ima yeni bir maddeyi üreten tek geçerli çıkarım kuralı olan hükümlerin tamamlayıcı değişmezleri içeren. Bir hazır bilgi , bir önerme değişkeni veya bir önerme değişkeninin olumsuzlanmasıdır. Biri diğerinin olumsuzlamasıysa, iki değişmezin tamamlayıcı olduğu söylenir (aşağıda tamamlayıcısı olarak alınır ). Ortaya çıkan yan tümce, tamamlayıcısı olmayan tüm değişmezleri içerir. Resmi olarak: ${\görüntüleme stili \l değil}$${\görüntüleme stili c}$

${\displaystyle {\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{ 1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}}$

nerede

all , , ve değişmezdir,${\ Displaystyle a_{i}}$${\displaystyle b_{i}}$${\görüntüleme stili c}$

bölen çizgi "anlamına gelir gerektirir ".

Yukarıdakiler şu şekilde de yazılabilir:

${\displaystyle {\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \ cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}}$

Çözünürlük kuralı tarafından üretilen maddeye , iki girdi maddesinin çözücüsü denir . Terimlerden ziyade maddelere uygulanan fikir birliği ilkesidir .

İki tümce birden fazla tamamlayıcı hazır bilgi çifti içerdiğinde, çözüm kuralı bu tür her bir çift için (bağımsız olarak) uygulanabilir; ancak sonuç her zaman bir totolojidir .

Modus ponens , çözümlemenin özel bir durumu olarak görülebilir (bir tek harfli tümce ve iki harfli tümce).

${\displaystyle {\frac {p\rightarrow q,\quad p}{q}}}$

eşdeğerdir

${\displaystyle {\frac {\p\lor q değil,\quad p}{q}}}$

Bir çözünürlük tekniği

Tam bir arama algoritması ile birleştiğinde , çözümleme kuralı , bir önerme formülünün tatmin edilebilirliğine karar vermek için sağlam ve eksiksiz bir algoritma ve buna ek olarak, bir aksiyom kümesi altında bir cümlenin geçerliliğini verir.

Bu çözümleme tekniği, çelişki yoluyla ispat kullanır ve önerme mantığındaki herhangi bir cümlenin, bağlaçlı normal formda eşdeğer bir cümleye dönüştürülebileceği gerçeğine dayanır . Adımlar aşağıdaki gibidir.

• Bilgi tabanındaki tüm cümleler ile ispat edilecek tümcenin ( varsayım ) olumsuzluğu bağlaçtır .
• Ortaya çıkan cümle, bağlaçların bir yan tümceler kümesinde ( S) öğeler olarak görülmesiyle birlikte normal bir bağlaç biçimine dönüştürülür .
  • Örneğin , kümeye yol açar .${\displaystyle (A_{1}\lor A_{2})\land (B_{1}\lor B_{2}\lor B_{3})\land (C_{1})}$${\displaystyle S=\{A_{1}\lor A_{2},B_{1}\lor B_{2}\lor B_{3},C_{1}\}}$
• Çözüm kuralı, tamamlayıcı değişmezleri içeren tüm olası tümce çiftlerine uygulanır. Çözüm kuralının her uygulamasından sonra, tekrarlanan değişmezler kaldırılarak elde edilen cümle basitleştirilir. Tümce tamamlayıcı değişmezler içeriyorsa, atılır (totoloji olarak). Değilse henüz hüküm seti mevcut değilse ve S , bu ilave edilir S ve ayrıca çözünürlük çıkarım için kabul edilir.
• Bir çözünürlük kural uygulandıktan sonra ise boş maddesi elde edilir, orijinal formülü edilemezdir (veya zıt ), ve yüzden, ilk tahmin sonucuna varılabilir izler aksiyomlardan.
• Öte yandan, boş tümce türetilemezse ve daha fazla yeni tümce türetmek için çözümleme kuralı uygulanamazsa, varsayım orijinal bilgi tabanının bir teoremi değildir.

Bu algoritmanın bir örneği , daha sonra çözücülerin açık temsili ihtiyacını ortadan kaldıran DPLL algoritmasına rafine edilmiş orijinal Davis-Putnam algoritmasıdır .

Çözünürlük tekniğinin bu açıklaması, çözünürlük türevlerini temsil etmek için temel veri yapısı olarak bir S kümesini kullanır . Listeler , Ağaçlar ve Yönlendirilmiş Döngüsel Grafikler diğer olası ve yaygın alternatiflerdir. Ağaç temsilleri, çözümleme kuralının ikili olduğu gerçeğine daha sadıktır. Cümleler için sıralı bir gösterimle birlikte, bir ağaç temsili, çözünürlük kuralının atomik kesme formülleriyle sınırlı , kesme kuralının özel bir durumuyla nasıl ilişkili olduğunu görmeyi de netleştirir . Bununla birlikte, ağaç temsilleri, küme veya liste temsilleri kadar kompakt değildir, çünkü bunlar, boş yan tümcenin türetilmesinde birden fazla kez kullanılan tümcelerin gereksiz alt türevlerini açıkça gösterir. Grafik gösterimleri, liste gösterimleri kadar madde sayısı bakımından kompakt olabilir ve ayrıca her bir çözücüyü türetmek için hangi maddelerin çözümlendiğine ilişkin yapısal bilgileri depolar.

Basit bir örnek

${\displaystyle {\frac {a\vee b,\quad \neg a\vee c}{b\vee c}}}$

Sade bir dille: Farz edelim ki yanlış. Öncülün doğru olması için doğru olması gerekir. Alternatif olarak, varsayalım doğrudur. Öncülün doğru olması için doğru olması gerekir. Bu nedenle, yanlışlığı veya doğruluğu ne olursa olsun, her iki öncül de geçerliyse , sonuç doğrudur. ${\görüntüleme stili bir}$${\görüntüleme stili a\vee b}$${\görüntüleme stili b}$${\görüntüleme stili bir}$${\görüntüleme stili \neg a\vee c}$${\görüntüleme stili c}$${\görüntüleme stili bir}$${\görüntüleme stili b\vee c}$

Birinci dereceden mantıkta çözünürlük

Çözünürlük kuralı, birinci dereceden mantığa genelleştirilebilir :

${\displaystyle {\frac {\Gamma _{1}\cup \left\{L_{1}\right\}\,\,\,\,\Gamma _{2}\cup \left\{L_{2 }\right\}}{(\Gamma _{1}\cup \Gamma _{2})\phi }}\phi }$

nerede bir olduğunu en genel birleştiricidir ait ve ve ve ortak değişkenler var. ${\görüntüleme stili\phi }$${\görüntüleme stili L_{1}}$${\displaystyle {\overline {L_{2}}}}$${\görüntüleme stili \Gama _{1}}$${\displaystyle \Gama _{2}}$

Örnek

Cümleleri ve bu kuralı birleştirici olarak uygulayabilir . ${\görüntüleme stili P(x),Q(x)}$${\görüntüleme stili \neg P(b)}$${\görüntüleme stili [b/x]}$

Burada x bir değişkendir ve b bir sabittir.

${\displaystyle {\frac {P(x),Q(x)\,\,\,\,\neg P(b)}{Q(b)}}[b/x]}$

Burada görüyoruz ki

• Cümleler ve çıkarımın öncülleridir${\görüntüleme stili P(x),Q(x)}$${\görüntüleme stili \neg P(b)}$
• ${\görüntüleme stili Q(b)}$ (tesislerin çözücüsü) onun sonucudur.
• Değişmez sol çözümlenmiş değişmezdir,${\görüntüleme stili P(x)}$
• Değişmez doğru çözümlenmiş değişmezdir,${\görüntüleme stili \neg P(b)}$
• ${\görüntüleme stili P}$ çözümlenmiş atom veya pivottur.
• ${\görüntüleme stili [b/x]}$ çözümlenmiş değişmezlerin en genel birleştiricisidir.

Resmi olmayan açıklama

Birinci dereceden mantıkta, çözümleme , mantıksal çıkarımın geleneksel kıyaslarını tek bir kurala indirger.

Çözünürlüğün nasıl çalıştığını anlamak için, aşağıdaki örnek mantık terim tasımını göz önünde bulundurun :

Bütün Yunanlılar Avrupalı.

Homeros bir Yunandır.

Bu nedenle, Homer bir Avrupalı.

Veya daha genel olarak:

${\görüntüleme stili \forall xP(x)\Rightarrow Q(x)}$

${\görüntüleme stili P(a)}$

Öyleyse, ${\görüntüleme stili Q(a)}$

Çözümleme tekniğini kullanarak akıl yürütmeyi yeniden biçimlendirmek için, ilk olarak tümceler birleşik normal biçime (CNF) dönüştürülmelidir. Bu formda, tüm niceleme örtük hale gelir: değişkenler ( X , Y , ...) üzerindeki evrensel niceleyiciler , anlaşıldığı gibi basitçe atlanır, varoluşsal olarak nicelenen değişkenlerin yerini Skolem işlevleri alır .

${\görüntüleme stili \neg P(x)\vee Q(x)}$

${\görüntüleme stili P(a)}$

Öyleyse, ${\görüntüleme stili Q(a)}$

Öyleyse soru şu ki, çözümleme tekniği son cümleyi ilk ikisinden nasıl türetiyor? Kural basit:

• Aynı yüklemi içeren, bir tümcede olumsuzlanan, diğerinde olmayan iki tümce bulun.
• İki yüklem üzerinde bir birleştirme gerçekleştirin . (Birleştirme başarısız olursa, kötü bir yüklem seçimi yaptınız. Önceki adıma dönün ve tekrar deneyin.)
• Birleştirilmiş yüklemlerde bağlı olan herhangi bir ilişkisiz değişken, iki tümcedeki diğer yüklemlerde de yer alıyorsa, bunları orada da sınır değerleriyle (terimler) değiştirin.
• Birleştirilmiş yüklemleri atın ve iki tümceden kalanları, yine "∨" operatörünün de katıldığı yeni bir yan tümcede birleştirin.

Bu kuralı yukarıdaki örneğe uygulamak için, P yükleminin olumsuzlanmış biçimde gerçekleştiğini buluyoruz.

¬ P ( X )

birinci fıkrada ve olumsuzlanmamış biçimde

P ( a )

ikinci fıkrada. X , bağlı olmayan bir değişkendir, a ise bir sınır değeridir (terim). İkisini birleştirmek ikameyi üretir

X ↦ bir

Birleşik yüklemleri atmak ve bu ikameyi kalan yüklemlere uygulamak ( bu durumda sadece Q ( X ), şu sonucu verir:

S ( bir )

Başka bir örnek için, kıyas biçimini düşünün

Bütün Giritliler adalıdır.

Bütün adalılar yalancıdır.

Bu nedenle tüm Giritliler yalancıdır.

Veya daha genel olarak,

∀ X P ( X ) → Q ( X )

∀ X Q ( X ) → R ( X )

Bu nedenle, ∀ X P ( X ) → R ( X )

CNF'de öncüller şöyle olur:

¬ P ( X ) ∨ Q ( X )

¬ Q ( Y ) ∨ R ( Y )

(İkinci tümcedeki değişkenin, farklı tümcelerdeki değişkenlerin farklı olduğunu açıkça belirtmek için yeniden adlandırıldığını unutmayın.)

Şimdi, birinci yan tümcedeki Q ( X ) ile ikinci yan tümcedeki ¬ Q ( Y )'yi birleştirmek, X ve Y'nin zaten aynı değişken olduğu anlamına gelir . Bunu kalan maddelerde yerine koymak ve bunları birleştirmek şu sonucu verir:

¬ P ( X ) ∨ R ( X )

faktoring

Robinson tarafından tanımlandığı şekliyle çözümleme kuralı, yukarıda tanımlandığı gibi kararın uygulanmasından önce veya uygulama sırasında aynı maddede iki değişmezi birleştiren faktoringi de içeriyordu. Ortaya çıkan çıkarsama kuralı çürütme-tamdır, çünkü bir dizi tümce tatmin edici değildir, ancak ve ancak boş tümcenin faktoring ile geliştirilmiş yalnızca çözünürlük kullanılarak bir türevi varsa.

Boş tümceyi türetmek için çarpanlara ayırmanın gerekli olduğu bir tatmin edici olmayan yan tümce kümesine örnek:

${\displaystyle {\begin{array}{rlcl}(1):&P(u)&\lor &P(f(u))\\(2):&\lnot P(v)&\lor &P(f( w))\\(3):&\l değil P(x)&\lor &\l değil P(f(x))\\\end{dizi}}}$

Her madde iki değişmez değerden oluştuğundan, her olası çözücü de öyle. Bu nedenle, çarpanlara ayırmadan çözülerek, boş yan tümce asla elde edilemez. Faktoring kullanılarak, örneğin aşağıdaki gibi elde edilebilir:

${\displaystyle {\begin{array}{rll}(4):&P(u)\lor P(f(w))&{\text{(1) ve (2)'yi }}v=f ile çözerek (u)\\(5):&P(f(w))&{\text{(4) çarpanlarına ayırarak, }}u=f(w)\\(6) ile:&\lP(f(f) değil (w')))&{\text{(5) ve (3)'ü }}w=w',x=f(w')\\(7) ile çözerek:&{\text{yanlış}} &{\text{(5) ve (6)'yı }}w=f(w')\\\end{dizi}}} ile çözerek$

Tümleşik olmayan çözünürlük

Yukarıdaki çözümleme kuralının, başlangıç ​​formüllerinin yan tümce normal formda olmasını gerektirmeyen genellemeleri tasarlanmıştır .

Bu teknikler, temel olarak, ara sonuç formüllerinin insan tarafından okunabilirliğini korumanın önemli olduğunu kanıtlayan etkileşimli teoremde faydalıdır. Ayrıca yan tümce-forma dönüşüm sırasında birleşimsel patlamadan kaçınırlar ve bazen çözüm adımlarından tasarruf ederler.

Önerme mantığında klozal olmayan çözümleme

Önerme mantığı için Murray ve Manna ve Waldinger kuralı kullanır

${\displaystyle {\begin{array}{c}F[p]\;\;\;\;\;\;\;\;\;G[p]\\\hline F[{\textit { true}}]\lor G[{\textit {false}}]\\\end{dizi}}}$,

burada isteğe bağlı bir formül temsil eder, ihtiva eden bir formül belirtmektedir bir altformül olarak ve de değiştirerek yerleşik her bir olayda ile ; için de aynı şekilde . Çözücü kuralları gibi kullanılarak basitleştirilebilir amaçlanan gereksiz önemsiz çözücülere üreten önlemek amacıyla, vb kural sadece uygulanacaktır sahip en az bir "negatif" ve "pozitif" bir olayda ve sırasıyla. Murray, uygun mantıksal dönüşüm kurallarıyla desteklenirse bu kuralın tamamlandığını göstermiştir. ${\görüntüleme stili p}$${\ Displaystyle F[p]}$${\görüntüleme stili p}$${\displaystyle F[{\textit {true}}]}$${\ Displaystyle F[p]}$${\görüntüleme stili p}$${\displaystyle {\textit {doğru}}}$${\görüntüleme stili G}$${\displaystyle F[{\textit {true}}]\lor G[{\textit {false}}]}$${\displaystyle q\land {\textit {true}}\implies q}$${\görüntüleme stili p}$${\görüntüleme stili F}$${\görüntüleme stili G}$

Traugott kuralı kullanır

${\displaystyle {\begin{array}{c}F[p^{+},p^{-}]\;\;\;\;\;\;\;\;G[p]\\\hline F[G[{\textit {true}}],\lnot G[{\textit {false}}]]\\\end{dizi}}}$,

burada üsleri , oluşumlarının polaritesini gösterir. Birlikte ve daha önce olduğu gibi inşa edilir, formül her bir pozitif ve her bir negatif oluşumunu değiştirilmesi ile elde edilir içinde olan ve sırasıyla. Murray'in yaklaşımına benzer şekilde, çözücüye uygun basitleştirme dönüşümleri uygulanmalıdır. Formüllerde kullanılan tek bağlaçlar olması koşuluyla , Traugott kuralının eksiksiz olduğunu kanıtladı . ${\görüntüleme stili p}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {yanlış}}]}$${\displaystyle F[G[{\textit {true}}],\lnot G[{\textit {false}}]]}$${\görüntüleme stili p}$${\görüntüleme stili F}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {yanlış}}]}$${\displaystyle \land ,\lor ,\rightarrow ,\lnot }$

Traugott'un çözücüsü Murray'inkinden daha güçlü. Ayrıca, yeni ikili birleştiriciler getirmez, böylece tekrarlanan çözünürlükte yan tümceli forma yönelik bir eğilimden kaçınır. Bununla birlikte, bir küçüğü birden çok kez daha büyük ve/veya ile değiştirildiğinde formüller uzayabilir . ${\görüntüleme stili p}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {yanlış}}]}$

Önermesel olmayan çözümleme örneği

Örnek olarak, kullanıcı tarafından verilen varsayımlardan başlayarak

${\displaystyle {\begin{array}{rccc}(1):&a&\rightarrow &b\land c\\(2):&c&\rightarrow &d\\(3):&b\land d&\rightarrow &e\\(4 ):&\lnot (a&\rightarrow &e)\\\end{dizi}}}$

Murray kuralı bir çelişkiyi anlamak için şu şekilde kullanılabilir:

${\displaystyle {\begin{array}{rrclccl}(5):&({\textit {true}}\rightarrow d)&\lor &(a\rightarrow b\land {\textit {false}})&\ }}p=c\\(6):&(b\land {\textit {true}}\rightarrow e)&\ ile, &d\lor \lbir&{\mbox{(2) ve (1)'den değil anlamına gelir:&\ lor &({\textit {false}}\lor \lnot a)&\impares &(b\rightarrow e)\lor \lnot a&{\mbox{(3) ve (5)'ten, }}p=d ile \\(7):&(({\textit {true}}\rightarrow e)\lor \l değil a)&\lor &(a\rightarrow {\textit {false}}\land c)&\implies &e\ lor \lnot a\lor \lnot a&{\mbox{(6) ve (1)'den, }}p=b\\(8) ile:&(e\lor \lnot {\textit {true}}\lor \lnot {\textit {true}})&\lor &\lnot ({\textit {false}}\rightarrow e)&\&e&{\mbox{7 ve (4)'ten, }}p= ile ima eder a\\(9):&\lnot (a\rightarrow {\textit {true}})&\lor &{\textit {false}}&\implies &{\textit {false}}&{\mbox{from (4) ve (8), }}p=e\\\end{dizi}}} ile$

Aynı amaçla Traugott kuralı aşağıdaki gibi kullanılabilir:

${\displaystyle {\begin{array}{rcccl}(10):&a\rightarrow b\land ({\textit {true}}\rightarrow d)&\implies &a\rightarrow b\land d&{\mbox{ from ( 1) ve (2), }}p=c\\(11):&a\rightarrow ({\textit {true}}\rightarrow e)&\ifadesi &a\rightarrow e&{\mbox{(10)'dan ve (3), ile }}p=(b\land d)\\(12):&\lnot {\textit {true}}&\implies &{\textit {false}}&{\mbox{(11'den) ) ve (4), }}p=(a\rightarrow e)\\\end{dizi}}} ile$

Her iki kesintinin karşılaştırılmasından, aşağıdaki sorunlar görülebilir:

• Traugott'un kuralı daha keskin bir çözücü sağlayabilir: (1) ve (2)'yi çözen (5) ve (10)'u karşılaştırın .${\görüntüleme stili p=c}$
• Murray'in kuralı 3 yeni ayırma sembolü getirdi: (5), (6) ve (7)'de, Traugott'un kuralı ise herhangi bir yeni sembol getirmedi; Bu anlamda Traugott'un ara formülleri, Murray'inkinden daha çok kullanıcının tarzına benzer.
• Nedeniyle ikinci konuya, Traugott kuralı olarak kullanan, varsayım (4) 'de ima yararlanabilirsiniz olmayan atom formül adımında (12). Murray kuralları kullanılarak anlamsal olarak eşdeğer formül (7) elde edilmiş, ancak sözdizimsel biçiminden dolayı kullanılamamıştır .${\görüntüleme stili p}$ ${\ Displaystyle a\rightarrow e}$${\displaystyle e\lor \l değil\lor \l değil}$${\görüntüleme stili p}$

Birinci mertebeden mantıkta klozsuz çözünürlük

Birinci mertebeden yüklem mantığı için, Murray'in kuralı , sırasıyla farklı, ancak birleştirilebilir alt formüllere ve of ve ' a izin verecek şekilde genelleştirilmiştir . Eğer en genel birleştiricidir; ve daha sonra jeneralize resolvent olduğunu . Daha özel bir ikame kullanılırsa kural sağlam kalırken , tamlığı sağlamak için bu tür kural uygulamalarına gerek yoktur. ${\görüntüleme stili p_{1}}$${\ Displaystyle p_{2}}$${\görüntüleme stili F}$${\görüntüleme stili G}$${\görüntüleme stili\phi }$${\görüntüleme stili p_{1}}$${\ Displaystyle p_{2}}$${\displaystyle F\phi [{\textit {true}}]\lor G\phi [{\textit {false}}}]}$${\görüntüleme stili\phi }$

Traugott kuralı birkaç pairwise farklı subformulas izin genelleştirilmiş edilir ait ve içinde uzun olduğunca, en genel bir birleştiricidir ortak olduğunu varsayalım . Genelleştirilmiş çözücü, ana formüllere uygulandıktan sonra elde edilir , böylece önermesel versiyonu uygulanabilir hale getirir. Traugott'un tamlık kanıtı, bu tamamen genel kuralın kullanıldığı varsayımına dayanır; ve ile sınırlıysa kuralının tam kalıp kalmayacağı açık değildir . ${\displaystyle p_{1},\ldots ,p_{m}}$${\görüntüleme stili F}$${\displaystyle p_{m+1},\ldots,p_{n}}$${\görüntüleme stili G}$${\displaystyle p_{1},\ldots ,p_{n}}$${\görüntüleme stili\phi }$${\görüntüleme stili\phi }$${\displaystyle p_{1}=\cdots =p_{m}}$${\displaystyle p_{m+1}=\cdots =p_{n}}$

paramodülasyon

Paramodülasyon, yüklem sembolünün eşitlik olduğu cümle kümeleri üzerinde akıl yürütme için ilgili bir tekniktir . Yansıtıcı kimlikler dışında tümceciklerin tüm "eşit" versiyonlarını üretir. Paramodulation operasyonu olumlu sürer gelen bir eşitlik değişmezi içermelidir maddesi. Daha sonra bir arar içine bir subterm ile maddesini bu eşitlik bir tarafı ile birleştirir. Alt terim daha sonra eşitliğin diğer tarafı ile değiştirilir. Paramodülasyonun genel amacı, sistemi atomlara indirgemek, ikame ederken terimlerin boyutunu küçültmektir.

Uygulamalar

• KARİN
• GKC
• Su samuru
• Prover9
• SNARK
• SPAS
• Vampir
• Logictools çevrimiçi kanıtlayıcı

Ayrıca bakınız

• Yoğunlaştırılmış ayrılma  - çözünürlüğün önceki bir sürümü
• Endüktif mantık programlama
• Ters çözünürlük
• mantık programlama
• Analitik tablo yöntemi
• SLD çözünürlüğü
• Çözünürlük çıkarımı

Notlar

Referanslar

• Robinson , J. Alan (1965). "Çözüm İlkesine Dayalı Bir Makine Yönelimli Mantık". ACM Dergisi . 12 (1): 23–41. doi : 10.1145/321250.321253 .
• Leitsch, Alexander (1997). Çözünürlük Hesabı . Springer .
• Gallier, Jean H. (1986). Bilgisayar Bilimi için Mantık: Otomatik Teorem Kanıtlamanın Temelleri . Harper & Row Yayıncılar.
• Lee, Chin-Liang Chang, Richard Char-Tung (1987). Sembolik mantık ve mekanik teorem ispatı ([yeniden baskı] ed.). San Diego: Akademik Basın. ISBN'si 0-12-170350-9.

Dış bağlantılar

• Alex Sakharov. "Çözünürlük İlkesi" . Matematik Dünyası .
• Alex Sakharov. "Çözünürlük" . Matematik Dünyası .