Původní článek: https://www.cs.cornell.edu/gries/Logic/Calculational.html
Výpočtová výroková logika je produktem výzkumníků v oblasti formálního vývoje algoritmů. (Klikněte sem pro krátkou historii.) C je v pořádku a kompletní. Důraz v důkazech je na nahrazení rovných za rovné místo modus ponens. Rovnost, nebo ekvivalence, přebírá důležitou roli místo toho, aby byla bitovým hráčem, jako ve většině výrokových logik.
& používáme pro spojení, | pro disjunkci a ~ pro negaci (ne).
V našem zápisu b = c označuje rovnost pro b a c stejného typu, zatímco b == c, neboli ekvivalence, je definována pouze pro b a c typu boolean. Pro b a c typu boolean mají b = c a b == c stejný význam.
Jedním z důvodů, proč mít dva symboly pro rovnost nad booleovskými symboly, je to, že rovnost = je obvykle považována za spojka :
b = c = d je zkratka pro b = c & c = d
zatímco b == c lze použít asociativně , což je pro nás velmi důležité:
b == c == d se rovná b == (c == d) ak (b == c) == d.
Níže je typický důkaz ve výpočtové logice. Čísla řádků jsou uvedena pouze pro pozdější diskusi. Tento příklad je vybrán, protože je jednoduchý, ale ukazuje všechny aspekty formálního systému důkazů (jak bude diskutováno později). Čísla teorémů odkazují na teorémy Logického přístupu k diskrétní matematice . Asociativnost a symetrie operátorů jsou řešeny transparentně, bez zmínky; to má za následek velké snížení počtu předkládaných vět a zjednodušuje manipulaci. Nakonec si všimněte, že styl je pouze formalizací stylu výpočtu používaného ve středoškolské algebře a skutečně mnoha vědci ve své práci - proto je styl tak užitečný.
Zde je důkaz ~p == p == false.
(0) ~p == p == nepravda
(1) = < (3,9), ~(p == q) == ~p == q , přičemž q:= p >
(2) ~(p == p ) == nepravda
(3) = < Identita == (3.9), přičemž q:= p >
(4) ~pravda == nepravda---(3.8)
Odvozovací pravidla výpočtové logiky
Zde jsou čtyři odvozená pravidla logiky C. (P[x:= E] označuje textovou substituci výrazu E za proměnnou x ve výrazu P):
- Substituce: Je-li P věta, pak je i P[x:= E].
|- P ---> |- P[x:= E]
- Leibniz: Jestliže P = Q je věta, pak je také E[x:= P] = E[x:= Q].
|- P = Q ---> |- E[x:= P] = E[x:= Q]
- Tranzitivita: Jestliže P = Q a Q = R jsou věty, pak platí i P = R.
|- P = Q, |- Q = R ---> |- P = R
- Rovnováha: Jestliže P a P == Q jsou věty, pak je Q také.
|- P, |- P == Q ---> |- Q
Vysvětlení formátu důkazu
Vysvětlíme, jak se čtyři odvozovací pravidla používají v důkazech, pomocí důkazu ~p == p == false.
(0) ~p == p == nepravda
(1) = < (3,9), ~(p == q) == ~p == q , přičemž q:= p >
(2) ~(p == p) == nepravda
(3) = < Identita == (3.9), s q:= p >
(4) ~pravda == nepravda ---(3.8)
Za prvé, řádky (0)-(2) ukazují použití odvozovacího pravidla Leibniz:
(0) = (2)
je Leibnizův závěr a jeho premisa ~(p == p) == ~p == p je uvedena na řádku (1). Stejným způsobem je rovnost na řádcích (2)-(4) doložena pomocí Leibnize.
"Nápověda" na řádku (1) má poskytnout Leibnizův předpoklad, který ukazuje, jaká náhrada rovných za rovné se používá. Touto premisou je věta (3.9) se substitucí p:= q, tzn
(~(p == q) == ~p == q)[p:=q]
To ukazuje, jak se v nápovědách používá inferenční pravidlo Substitution.
Z (0) = (2) a (2) = (4) usuzujeme pomocí inferenčního pravidla Tranzitivita, že (0) = (4). To ukazuje, jak se používá Transitivity.
Nakonec si všimněte, že řádek (4), ~pravda == nepravda, je teorém, jak naznačuje nápověda napravo. Odvozovacím pravidlem Rovnováha tedy docházíme k závěru, že přímka (0) je také věta. A (0) je to, co jsme chtěli dokázat.
Tento formát nátisku má několik výhod.
- Použití každého odvozovacího pravidla je určeno formátem důkazu, takže názvy odvozovacích pravidel není třeba uvádět. To snižuje množství čtení a psaní v důkazu.
- Důkaz je zcela přísný, ale bez zdrcující složitosti. Dále je důkaz dostatečně jednoduchý, aby jej studenti pochopili. Ve skutečnosti formalizuje styl výpočtu vyučovaný na střední škole.
- Obecně platí, že existuje malé kopírování vzorců z jednoho řádku na druhý -- jedna z nevýhod Hilbertových důkazů.
- S tímto formátem lze učit užitečné principy a strategie důkazů.
- Důkaz lze číst dopředu nebo dozadu.