Uvod u računsku logiku

Orginalni članak: https://www.cs.cornell.edu/gries/Logic/Calculational.html

Računska propozicijska logika proizvod je istraživača u području formalnog razvoja algoritama. ( Kliknite ovdje za kratku povijest .) C je zdrav i potpun. Naglasak u dokazima je na zamjeni jednakog za jednako, umjesto na modus ponens. Jednakost, ili ekvivalencija, preuzima važnu ulogu umjesto da bude bitni igrač, kao u većini iskaznih logika.

Koristimo & za spoj, | za disjunkciju, a ~ za negaciju (ne).

U našem zapisu, b = c označava jednakost, za b i c istog tipa, dok je b == c, ili ekvivalentnost, definirana samo za b i c tipa boolean. Za b i c tipa boolean, b = c i b == c imaju isto značenje.

Jedan od razloga za postojanje dvaju simbola za jednakost u odnosu na booleove je taj što se jednakost = obično promatra kao veznik :

b = c = d je skraćenica za b = c & c = d

dok se b == c može koristiti asocijativno , što je za nas od velike važnosti:

b == c == d jednako je b == (c == d) i (b == c) == d.

Dolje je tipičan dokaz u računskoj logici. Brojevi redaka prisutni su samo za kasniju raspravu. Ovaj primjer je odabran jer je jednostavan, ali pokazuje sve aspekte formalnog sustava dokazivanja (kao što će biti objašnjeno kasnije). Brojevi teorema odnose se na teoreme Logičkog pristupa diskretnoj matematici . Asocijativnost i simetričnost operatora tretiraju se transparentno, bez spominjanja; ovo rezultira velikim smanjenjem broja teorema koje treba predstaviti i pojednostavljuje manipulaciju. Naposljetku, imajte na umu da je stil samo formalizacija stila izračuna koji se koristi u srednjoškolskoj algebri, kao i mnogi znanstvenici u svom radu -- zato je stil tako koristan.

Ovdje je dokaz ~p == p == false .

(0) ~p == p == netočno
(1) = < (3.9), ~(p == q) == ~p == q , s q:= p >
(2) ~(p == p ) == false
(3) = < Identitet == (3.9), s q:= p >
(4) ~true == false --(3.8)

Pravila zaključivanja računske logike

Ovdje su četiri pravila zaključivanja logike C. (P[x:= E] označava tekstualnu zamjenu izraza E za varijablu x u izrazu P):

• Zamjena: Ako je P teorem, onda je i P[x:= E].

|- P ---> |- P[x:= E]

• Leibniz: Ako je P = Q teorem, onda je i E[x:= P] = E[x:= Q].

|- P = Q ---> |- E[x:= P] = E[x:= Q]

• Tranzitivnost: Ako su P = Q i Q = R teoremi, onda je i P = R.

|- P = Q, |- Q = R ---> |- P = R

• Ravnomjernost: Ako su P i P == Q teoremi, onda je i Q.

|- P, |- P == Q ---> |- Q

Objašnjenje formata dokaza

Objašnjavamo kako se četiri pravila zaključivanja koriste u dokazima, koristeći dokaz ~p == p == false .

(0) ~p == p == netočno

(1) = < (3.9), ~(p == q) == ~p == q , s q:= p >

(2) ~(p == p) == lažno

(3) = < Identitet == (3.9), s q:= p >

(4) ~true == false ---(3.8)

Prvo, linije (0)-(2) pokazuju korištenje Leibnizova pravila zaključivanja:

(0) = (2)

je zaključak Leibniza, a njegova premisa ~(p == p) == ~p == p dana je u retku (1). Na isti način, jednakosti na pravcima (2)-(4) potvrđuju se pomoću Leibniza.

"Savjet" u retku (1) trebao bi dati Leibnizovu premisu, pokazujući kakva se zamjena jednakog za jednako koristi. Ova premisa je teorem (3.9) sa zamjenom p:= q, tj

(~(p == q) == ~p == q)[p:=q]

Ovo pokazuje kako se pravilo zaključivanja Zamjena koristi unutar savjeta.

Iz (0) = (2) i (2) = (4), pravilom zaključivanja tranzitivnosti zaključujemo da je (0) = (4). Ovo pokazuje kako se koristi tranzitivnost.

Na kraju, primijetite da je red (4), ~true == false, teorem, kao što je naznačeno savjetom s desne strane. Stoga, prema pravilu zaključivanja Equanimity, zaključujemo da je pravac (0) također teorem. A (0) je ono što smo htjeli dokazati.

Ovaj format dokaza ima nekoliko prednosti.

• Korištenje svakog pravila zaključivanja određeno je formatom dokaza, tako da nazive pravila zaključivanja ne treba spominjati. To smanjuje količinu čitanja i pisanja u korekturi.
• Dokaz je potpuno rigorozan, ali bez pretjerane složenosti. Nadalje, dokaz je dovoljno jednostavan da ga studenti mogu razumjeti. Zapravo, formalizira stil računanja koji se uči u srednjoj školi.
• Općenito, malo je kopiranja formula iz jednog retka u drugi - jedan od nedostataka dokaza u Hilbertovom stilu.
• Pomoću ovog formata mogu se poučavati korisni principi i strategije dokazivanja.
• Dokaz se može čitati unaprijed ili unatrag.