Ad argvmentvm transi
Topos Uranos
Latine

Algorithmvs formarvm normalivm eivsqve vsvs

Svmmarivm

Lectio de formis normalibvs demonstravit omnem formvlam formae normali disivnctivae et conivnctivae aeqvivalere; haec docet qvomodo eae sine tabvla compvtentvr et qvomodo eis vtendvm sit. Compvtatio est algorithmvs rescribendi tribvs phasibvs constans: implicatio dvplex, disivnctio exclvsiva, negatio conivncta et implicatio tollvntvr; negationes legibvs De Morgani et dvplici negatione vsqve ad variabiles dedvcvntvr; et distribvitvr, conivnctio svper disivnctionem ad formam disivnctivam et disivnctio svper conivnctionem ad conivnctivam. Demonstrantvr eivs rectitvdo, qvae ex svbstitvtione semantica seqvitvr, et eivs terminatio, mensvra nvmerica adhibita qvae in omni passv omnis phasis decrescit; et demonstratvr etiam eivs limes: forma conivnctiva disivnctionis nn conivnctionvm dvarvm variabilivm necessario 2n2^n clavsvlas habet. Deinde formae normales ex tabvla veritatis instrvmenti cvivs interiora non videntvr elicivntvr, versibvs vicinis conflandis simplificantvr et in circvitvs interrvptorvm in serie et in parallelo convertvntvr. Problema instrvmenti qvattvor interrvptorvm plane solvitvr, cvm tabvla sva, dvabvs formis et circvitibvs; problema qvinqve interrvptorvm provocationis loco relinqvitvr.

Proposita discendi

  1. Algorithmvm rescribendi adhibere vt forma normalis disivnctiva et conivnctiva formvlae obtineantvr, eam implicationis dvplicis eliminationem eligendo qvae loco in qvo occvrrit convenit.
  2. Demonstrare algorithmvm rectvm esse, per svbstitvtionem semanticam, et terminari, mensvris adhibitis qvae in omni passv decrescvnt; et exponere cvr forma conivnctiva exponentialiter longior esse possit qvam formvla a qva proficiscitvr.
  3. Formas normales capsae nigrae ex eivs tabvla veritatis constrvere easqve versibvs vicinis conflandis simplificare.
  4. Circvitvs interrvptorvm in serie et in parallelo per formvlas repraesentare, et circvitvs designare ac simplificare qvi praescriptioni sermone natvrali datae satisfaciant.

Lectio de formis normalibvs dvas earvm exsistentiae demonstrationes dedit. Prima per tabvlam veritatis procedit, qvae 2n2^n versvs pro nn variabilibvs habet; altera formvlam a variabilibvs percvrrit, vnicam eivs regvlam formationis secvta. Nevtra dicit qvomodo agendvm sit cvm formvla implicationibvs, implicationibvs dvplicibvs et negationibvs inter se insertis scripta, qvo modo formvlae plervmqve se praebent. Si hoc ita est, deest ratio qvae in ipsa scriptvra operetvr, qvae sine cogitatione exseqvi possit, qvam terminari constet et qvae formvlam aeqvivalentem reddat. Id est algorithmvs, et eivs stvdivm primvm hvivs lectionis obiectvm est; altervm est qvod eo efficitvr: instrvmenti agendi modvm formvlis describere et circvitvm constrvere qvi evm reddat.

Scriptvrae et svbstitvtio

Meminerimvs formvlas cvrsvs catenas circvlorvm et discorvm esse, et ¬\neg, ∨\vee, ∧\wedge, →\rightarrow, ↔\leftrightarrow et ⊻\veebar abbreviationes esse ex negatione conivncta definitas (lectio de lingva logicae propositionalis). Cvm ((p∨q)→(¬q∧p))((p \vee q) \rightarrow (\neg q \wedge p)) scribimvs, non catenam scribimvs, sed eivs scriptvram: arborem cvivs folia variabiles svnt et cvivs nodi connectiva ¬\neg, ∧\wedge, ∨\vee, →\rightarrow, ↔\leftrightarrow, ⊻\veebar et ↓\downarrow svnt, vnvmqvodqve cvm partibvs svis. Omnis scriptvra vnam formvlam designat, eam qvae explicandis eivs abbreviationibvs oritvr; et vna eademqve formvla plvres scriptvras habere potest: lectio de formis normalibvs animadvertit ¬¬φ\neg\neg\varphi et (φ∨φ)(\varphi \vee \varphi) eandem catenam esse. Algorithmvs scriptvram legit, non catenam; qvare eas distingvere expedit. Cvm distinctio eo tantvm valeat vt sciatvr vbi qvisqve passvs agat, litteris φ\varphi, ψ\psi, χ\chi vtemvr et pro scriptvris et pro formvlis qvas designant, et φ≡ψ\varphi \eqsem \psi scribemvs cvm formvlae designatae semantice aeqvivalentes svnt. Svbscriptvra scriptvrae est arbor minor qvae ex vno eivs nodorvm pendet.

Passvs algorithmi vnam svbscriptvram alia svbstitvit. Instrvmentvm qvod praestat hanc mvtationem significationem non mvtare est theorema svbstitvtionis semanticae lectionis de conseqventia et aeqvivalentia semanticis; sed illvd theorema vnam occvrrentiam in catena svbstitvit, et svbscriptvrae plvres occvrrentiae in catena respondere possvnt, qvia omnis abbreviatio partes svas iterat: in (φ∨ψ)=((φ↓ψ)↓(φ↓ψ))(\varphi \vee \psi) = ((\varphi \downarrow \psi) \downarrow (\varphi \downarrow \psi)), pars φ\varphi bis apparet. Lemma seqvens svbstitvtionem ad scriptvras accommodat.

LemmaSvbstitvtio in scriptvra

Sit χ\chi scriptvra, θ\theta vna ex eivs svbscriptvris et θ′\theta' scriptvra cvm θ≡θ′\theta \eqsem \theta'. Si χ′\chi' oritvr cvm in χ\chi illa svbscriptvra per θ′\theta' svbstitvitvr, tvm χ≡χ′\chi \eqsem \chi'.

Demonstratio

  1. χ′=θ′≡θ=χ\chi' = \theta' \eqsem \theta = \chi

    Per indvctionem in profvnditate nodi ex qvo θ\theta pendet, id est in nvmero connectivorvm ipsivs χ\chi qvae svpra evm svnt. Si profvnditas est 00, svbscriptvra est tota scriptvra.

  2. χ=c(χ1,χ2),χ′=c(χ1′,χ2),χ1′≡χ1\dato{hi}{\chi = c(\chi_1, \chi_2), \qquad \chi' = c(\resaltar{\chi_1'}, \chi_2), \qquad \chi_1' \eqsem \chi_1}

    Si maior est qvam 00, radix ipsivs χ\chi est connectivvm cc cvm partibvs χ1\chi_1 (et χ2\chi_2, si cc dvorvm argvmentorvm est), et θ\theta ex vna earvm pendet, pvta χ1\chi_1, minore profvnditate. Per hypothesin indvctionis, mvtatio intra χ1\chi_1 scriptvram aeqvivalentem reddit.

  3. v(χ′)=Fc(v(χ1′),v(χ2))=Fc(v(χ1),v(χ2))=v(χ)v(\chi') = F_c\left( v(\chi_1'), v(\chi_2) \right) = F_c\left( v(\chi_1), v(\chi_2) \right) = v(\chi)

    Per theorema de valoribvs connectivorvm derivatorvm (lectio de semantica logicae propositionalis) et per clavsvlam negationis conivnctae, valor ipsivs c(χ1,χ2)c(\chi_1, \chi_2) in aestimatione fvnctio est valorvm ipsorvm χ1\chi_1 et χ2\chi_2, et hi non mvtantvr. Ergo χ\chi et χ′\chi' in omni aestimatione evndem valorem habent.

Hic FcF_c est fvnctio veritatis connectivi: F¬(a)=1−aF_\neg(a) = 1 - a, F∧(a,b)=abF_\wedge(a, b) = ab, et similiter pro ceteris. Idem effectvm ex theoremate svbstitvtionis semanticae obtinetvr, si semel pro vnoqvoqve exemplari ipsivs θ\theta in catena adhibetvr et aeqvivalentiae per transitivitatem concatenantvr; demonstratio per scriptvram brevior est, qvia connectiva scripta nvmerat, non exemplaria.