Bevezetés a számítási logikába

Eredeti cikk: https://www.cs.cornell.edu/gries/Logic/Calculational.html

A kalkulációs propozíciós logika az algoritmusok formális fejlesztésének területén kutató kutatók terméke. (Kattintson ide a rövid előzményekért.) A C hang és teljes. A bizonyításokban a hangsúly az egyenlők egyenlőkkel való helyettesítésén van a modus ponens helyett. Az egyenlőség vagy az ekvivalencia fontos szerepet tölt be ahelyett, hogy kicsit játékos lenne, mint a legtöbb propozíciós logikában.

Az & kötőszót használjuk , | diszjunkcióra, és ~ tagadására (nem).

A mi jelölésünkben a b = c egyenlőséget jelöl az azonos típusú b és c esetén, míg a b == c vagy ekvivalencia csak a logikai típusú b és c esetén van definiálva. Boolean típusú b és c esetén a b = c és a b == c jelentése ugyanaz.

Az egyik oka annak, hogy a logikai értékekkel szemben két egyenlőséget jelző szimbólum van, az az, hogy az egyenlőséget = általában úgy tekintik, mint kötőszó :

b = c = d a b = c és c = d rövidítése

míg a b == c asszociatívan használható , ami nagyon fontos számunkra:

b == c == d egyenlő b == (c == d) és (b == c) == d értékkel.

Az alábbiakban egy tipikus bizonyítást mutatunk be a számítási logikában. A sorszámok csak későbbi megbeszélés céljából jelennek meg. Ezt a példát azért választottuk, mert egyszerű, de bemutatja a formális bizonyítási rendszer minden aspektusát (amint azt később tárgyaljuk). A tételszámok A diszkrét matematika logikai megközelítése tételekre vonatkoznak . Az operátorok asszociativitását és szimmetriáját átláthatóan kezeljük, említés nélkül; ez a bemutatandó tételek számának nagymértékű csökkenését eredményezi, és leegyszerűsíti a manipulációt. Végezetül vegye figyelembe, hogy a stílus csak a középiskolai algebrában használt számítási stílus formalizálása, és valóban sok tudós munkája során – ezért olyan hasznos a stílus.

Itt van a ~p == p == false bizonyítéka.

(0) ~p == p == hamis
(1) = < (3.9), ~(p == q) == ~p == q , q:= p >
(2) ~(p == p ) == hamis
(3) = < == (3.9) azonossága , q:= p >
(4) ~igaz == hamis ---(3.8)

A számítási logika következtetési szabályai

Íme a C logika négy következtetési szabálya . (P[x:= E] az E kifejezés szöveges helyettesítését jelöli az x változóval a P kifejezésben):

• Behelyettesítés: Ha P tétel, akkor P[x:= E] is: |- P ---> |- P[x:= E]
• Leibniz: Ha P = Q tétel, akkor az E[x:= P] = E[x:= Q] is: |- P = Q ---> |- E[x:= P] = E[x:= Q]
• Tranzitivitás: Ha P = Q és Q = R tételek, akkor P = R is: |- P = Q, |- Q = R ---> |- P = R
• Egyenlőség: Ha P és P == Q tételek, akkor Q is az: |- P, |- P == Q ---> |- Q

A bizonyítási formátum magyarázata

Elmagyarázzuk, hogyan használják a négy következtetési szabályt a bizonyításokban, a ~p == p == false bizonyításával .

(0) ~p == p == hamis

(1) = < (3,9), ~(p == q) == ~p == q , q:= p >

(2) ~(p == p) == hamis

(3) = < == azonossága (3.9), q:= p >

(4) ~igaz == hamis ---(3,8)

Először is, a (0)-(2) sorok a Leibniz következtetési szabály használatát mutatják:

(0) = (2)

Leibniz következtetése, és a ~(p == p) == ~p == p premisszája az (1) vonalon van megadva. Ugyanígy a (2)-(4) egyenesek egyenlőségét Leibniz segítségével igazoljuk.

Az (1) sorban található „tipp” feltehetően Leibniz premisszáját adja, megmutatva, hogy az egyenlők egyenlő helyett milyen helyettesítést használnak. Ez az előfeltevés a (3.9) tétel p:= q behelyettesítéssel, azaz

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

Ez azt mutatja meg, hogyan használják a következtetési szabályt a Helyettesítés a tippekben.

A (0) = (2) és (2) = (4) alapján a Tranzitivitás következtetési szabályával arra következtetünk, hogy (0) = (4). Ez megmutatja, hogyan használják a tranzitivitást.

Végül vegye figyelembe, hogy a (4) sor, ~igaz == hamis, egy tétel, amint azt a jobb oldali utalás jelzi. Ezért az Egyenlőség következtetési szabályával arra a következtetésre jutunk, hogy a (0) egyenes is egy tétel. És (0) ezt akartuk bizonyítani.

Ennek a bizonyítási formátumnak számos előnye van.

• Az egyes következtetési szabályok használatát a bizonyítási formátum határozza meg, így a következtetési szabályok nevét nem kell megemlíteni. Ez csökkenti az olvasás és az írás mennyiségét a bizonyításban.
• A bizonyítás teljesen szigorú, de bonyolultság nélkül elsöprő. Ezenkívül a bizonyítás elég egyszerű ahhoz, hogy a tanulók megértsék. Valójában formalizálja a középiskolában tanított számítási stílust.
• Általában kevés a képletek egyik sorból a másikba másolása – ez a Hilbert-stílusú bizonyítások egyik hátránya.
• Ezzel a formátummal hasznos bizonyítási elvek és stratégiák taníthatók.
• A bizonyítás előre és hátra is olvasható.