Ad argvmentvm transi
Topos Uranos
Latine

Methodvs resolvtionis

Svmmarivm

Semantica methodos promiserat ad insatisfactibilitatem decernendam qvae tabvlam veritatis non percvrrerent; haec lectio praecipvam earvm tradit. Classis formvlarvm vt classis clavsvlarvm scribitvr, qvarvm qvaeqve classis finita litteralivm est, per formam normalem conivnctivam vel, vt eivs incrementvm exponentiale vitetvr, per clavsvlas definitionis cvm variabilibvs novis, qvae satisfactibilitatem servant. In clavsvlas vna sola regvla agit, resolvtionis: ex clavsvla qvae litterale continet et altera qvae eivs oppositvm continet infertvr vnio vtrivsqve sine eo pari. Refvtatio est derivatio qvae ad clavsvlam vacvam pervenit. Demonstrantvr firmitas (si refvtatio est, classis insatisfactibilis est), per indvctionem in longitvdine derivationis, et completvdo refvtationis (si classis finita insatisfactibilis est, refvtatio est), per indvctionem in nvmero variabilivm, qvae singvlae eliminantvr; theoremate compactitatis completvdo ad classes infinitas extenditvr. Inde oritvr methodvs ad conseqventias decernendas, qvae cvm tabvlis comparatvr, et expositio qvaestionis satisfactibilitatis, cvm dvobvs casibvs qvi celeriter decernvntvr: clavsvlis Hornianis et clavsvlis dvorvm litteralivm.

Proposita discendi

  1. Classem formvlarvm vt classem clavsvlarvm repraesentare, per formam normalem conivnctivam vel per clavsvlas definitionis cvm variabilibvs novis, et ostendere repraesentationem satisfactibilitatem et conseqventiam servare.
  2. Refvtationes per resolvtionem constrvere et iis conseqventias et insatisfactibilitatem decernere, errores typicos vitando, vt dvo paria complementaria vna illatione eliminare.
  3. Firmitatem resolvtionis per indvctionem in longitvdine derivationvm et eivs completvdinem refvtationis per eliminationem variabilivm demonstrare, eamqve ad classes infinitas theoremate compactitatis extendere.
  4. Qvaestionem satisfactibilitatis, eivs svmptvm notvm et casvs qvi celeriter decernvntvr (clavsvlas Hornianas et clavsvlas dvorvm litteralivm) exponere, et resolvtionem cvm tabvlis veritatis comparare.

Lectio de semantica logicae propositionalis ostendit validitatem et satisfactibilitatem per tabvlam veritatis decerni posse, svmptv qvi cvm singvlis variabilibvs dvplicatvr, et methodos promisit qvae eam percvrrere non postvlarent. Lectio de conseqventia et aeqvivalentia semanticis omnem conseqventiam ad insatisfactibilitatem redvxit: Γ⊨φ\Gamma \models \varphi si et solvm si Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} insatisfactibilis est. Lectiones de formis normalibvs et de earvm algorithmo omni formvlae formam conivnctivam dedervnt, cvivs validitas primo aspectv cernitvr, satisfactibilitas avtem non cernitvr. Si ita est, deest procedvra qvae insatisfactibilitatem conivnctionis clavsvlarvm decernat in ipsis clavsvlis operando. Haec procedvra est resolvtio, a Ioanne Alano Robinson anno 1965 proposita ex ideis Martini Davis et Hilarii Pvtnam (1960); nvclevs est programmatvm qvae hodie satisfactibilitatem formvlarvm cvm milionibvs variabilivm decernvnt. Dissimiliter a systemate vnitatis de dedvctione, cvivs necessitvdines cvm semantica lectiones de firmitate et completvdine et de theoremate compactitatis investigant, resolvtio conclvsiones non dedvcit: classes refvtat. Haec lectio demonstrat eam id firme et complete facere.

Vt in lectionibvs prioribvs, pp, qq, rr, ss et tt variabiles v1v_1 ad v5v_5 nominant; littera vv sine indice, et etiam ww, aestimationes designant; et V(φ)V(\varphi) est classis variabilivm formvlae φ\varphi.

Clavsvlae et classes clavsvlarvm

Ex lectione de formis normalibvs memoretvr litterale esse variabilem vel negationem variabilis, et oppositvm litteralis ℓ\ell, qvod ℓ∗\ell^{*} scribitvr, esse litterale eivsdem variabilis et alterivs signi; dvo litteralia opposita par complementarivm facivnt. Per lemma de negatione litteralis, v(ℓ∗)=1−v(ℓ)v(\ell^{*}) = 1 - v(\ell) pro omni aestimatione vv. Ibi clavsvla erat disivnctio litteralivm; hic expedit ordinem et repetitiones, qvae valorem non mvtant, oblivisci et classem retinere.

Clavsvla est classis finita litteralivm. Clavsvla sine litteralibvs clavsvla vacva appellatvr et □\Box scribitvr. Aestimatio vv clavsvlae CC satisfacit, qvod v⊨Cv \models C scribitvr, si aliqvod litterale clavsvlae CC valet 11 in vv; sin minvs, vv eam refvtat. Clavsvla vnivs litteralis singvlaris appellatvr. Variabiles clavsvlae classem V(C)V(C) facivnt; variabiles classis SS clavsvlarvm classem V(S)V(S), vnionem priorvm. Aestimatio classi SS clavsvlarvm satisfacit, v⊨Sv \models S, si singvlis eivs clavsvlis satisfacit; SS satisfactibilis est si aliqva aestimatio ei satisfacit, et insatisfactibilis sin minvs. Deniqve, si SS classis clavsvlarvm est et CC clavsvla, S⊨CS \models C significat omnem aestimationem qvae classi SS satisfacit etiam clavsvlae CC satisfacere.

v⊨C  ⇔  (∃ℓ∈C)  v(ℓ)=1,v⊨S  ⇔  (∀C∈S)  v⊨Cv \models C \;\Leftrightarrow\; (\exists \ell \in C)\; v(\ell) = 1, \qquad v \models S \;\Leftrightarrow\; (\forall C \in S)\; v \models C

Dvo casvs extremi ex definitione seqvvntvr, qvos figere expedit. Clavsvla vacva litteralia non habet; ergo nvllvm eivs litterale valet 11, et nvlla aestimatio ei satisfacit: □\Box insatisfactibilis est, et omnis classis qvae eam continet item. Classis vacva clavsvlarvm, contra, clavsvlas qvibvs satisfaciendvm sit non habet, et omnis aestimatio ei satisfacit. Non svnt confvndendae: {□}\{\Box\} insatisfactibilis est, et classi ∅\emptyset omnes aestimationes satisfacivnt.

LemmaClavsvla et eivs disivnctio

Sit C={ℓ1,…,ℓk}C = \{\ell_1, \ldots, \ell_k\} clavsvla non vacva, cvivs litteralia qvolibet ordine et sine repetitione scripta svnt. Pro omni aestimatione vv, v⊨Cv \models C si et solvm si v(⋁j=1kℓj)=1v\left( \bigvee_{j=1}^{k} \ell_j \right) = 1. Praesertim omnes disivnctiones litteralivm clavsvlae CC, qvolibet ordine et cvm repetitionibvs, inter se aeqvivalent. Praeterea, omnis aestimatio clavsvlae CC satisfacit si et solvm si ea par complementarivm continet.

Demonstratio

  1. v(⋁j=1kℓj)=1  ⇔  (∃j≤k)  v(ℓj)=1v\left( \bigvee_{j=1}^{k} \ell_j \right) = 1 \;\Leftrightarrow\; (\exists j \leq k)\; v(\ell_j) = 1

    Per lemma valoris disivnctionvm nn formvlarvm, in lectione de legibvs De Morgani et legibvs distribvtivis generalibvs demonstratvm, disivnctio valet 11 si et solvm si aliqvis eivs terminvs valet 11.

  2. v(⋁j=1kℓj)=1  ⇔  v⊨Cv\left( \bigvee_{j=1}^{k} \ell_j \right) = 1 \;\Leftrightarrow\; \resaltar{v \models C}

    Aliqvod ℓj\ell_j valere 11 idem est ac aliqvod litterale clavsvlae CC valere 11, id est vv clavsvlae CC satisfacere. Condicio neqve ab ordine neqve a repetitionibvs pendet, qvia solvm qvaerit qvae litteralia insint.

  3. (∀v)  v⊨C  ⇔  (∃ℓ)  ℓ∈C,  ℓ∗∈C(\forall v)\; v \models C \;\Leftrightarrow\; (\exists \ell)\; \ell \in C, \; \ell^{*} \in C

    Per lemma de conivnctionibvs elementaribvs et clavsvlis (lectio de formis normalibvs), disivnctio litteralivm valida est si et solvm si par complementarivm continet; per ea qvae praecedvnt, idem de CC valet.

Clavsvla qvae par complementarivm continet tavtologica appellatvr: nvllam condicionem imponit, et ex qvalibet classe tolli potest eivs exemplaribvs non mvtatis. Clavsvlas vt classes scribere non est libido notationis. Si ex (p∨q)(p \vee q) et (p∨¬q)(p \vee \neg q) obtinere volvmvs pp, disivnctio dat (p∨p)(p \vee p), qvae formvlae pp aeqvivalet sed non eadem formvla est; cvm classibvs, {p}∪{p}={p}\{p\} \cup \{p\} = \{p\}, et conflatio litteralivm repetitorvm sponte fit.

ExemplvmClassi clavsvlarvm satisfacere

Sit S={{p,q},{¬p,r},{¬q}}S = \{ \{p, q\}, \{\neg p, r\}, \{\neg q\} \}. Clavsvla {¬q}\{\neg q\} postvlat v(q)=0v(q) = 0; deinde {p,q}\{p, q\} postvlat v(p)=1v(p) = 1, et deinde {¬p,r}\{\neg p, r\} postvlat v(r)=1v(r) = 1. Aestimatio qvae 11 dat variabilibvs pp et rr et 00 ceteris variabilibvs classi SS satisfacit, et vnica est possibilitas in V(S)={p,q,r}V(S) = \{p, q, r\}. Si clavsvla {¬r}\{\neg r\} additvr, nvlla aestimatio classi avctae satisfacit: insatisfactibilis est, qvamqvam □\Box non continet.

v(q)=0  ⇒  v(p)=1  ⇒  v(r)=1v(q) = 0 \;\Rightarrow\; v(p) = 1 \;\Rightarrow\; v(r) = 1