Toto je seznam pravidel inference, logických zákonů, které se vztahují k matematickým vzorcům.
Pravidla odvození jsou syntaktická transformační pravidla, která lze použít k vyvození závěru z premisy pro vytvoření argumentu. Soubor pravidel lze použít k vyvození jakéhokoliv platného závěru, pokud je úplný, přičemž nikdy nevyvodíme neplatný závěr, pokud je správný. Spolehlivý a úplný soubor pravidel nemusí obsahovat každé pravidlo v následujícím seznamu, protože mnoho pravidel je nadbytečných a lze je prokázat s ostatními pravidly.
Pravidla vypouštění umožňují vyvozovat závěry z subderivace založené na dočasném předpokladu. Níže, notace
označuje takové subderivace z dočasného předpokladu do .
Pravidla pro klasický sententiální počet
Sententiální kalkul je také znám jako výrokový kalkul.
Pravidla klasického predikátového počtu
V následujících pravidlech, je přesně jako s výjimkou toho, že termín všude má volné proměnné .
Omezení 1: nevyskytuje se v .
Omezení 2: není uvedeno v žádné hypotéze ani neuvedených předpokladech.
Omezení: Žádný volný výskyt v spadá do rozsahu kvantifikátoru kvantifikace proměnné vyskytující se v .
Omezení: Žádný volný výskyt v spadá do rozsahu kvantifikátoru kvantifikace proměnné vyskytující se v .
Omezení 1: Žádný volný výskyt v spadá do rozsahu kvantifikátoru kvantifikující proměnnou vyskytující se v .
Omezení 2: Neexistuje žádný výskyt, volný nebo vázaný, v .
Tabulka: Pravidla vlivu – krátké shrnutí
Výše uvedená pravidla lze shrnout do následující tabulky. Sloupec „Tautologie“ ukazuje, jak interpretovat notaci daného pravidla.
Všechna pravidla používají základní logické operátory. Úplnou tabulku „logických operátorů“ znázorňuje pravdivostní tabulka, která obsahuje definice všech možných (16) pravdivostních funkcí 2 booleovských proměnných (p, q):
kde T = true a F = false, a, sloupce jsou logické operátory: 0, false, Contradiction; 1, NOR, Logical NOR; 2, Converse nonimplication; 3, ¬p, Negation; 4, Material nonimplication; 5, ¬q, Negation; 6, XOR, Exclusive disjunction; 7, NAND, Logical NAND; 8, AND, Logical conjunction; 9, XNOR, If and only if, Logical biconditional; 10, q, Projection function; 11, if/then, Logical implication; 12, p, Projection function; 13, then/if, Converse implication; 14, OR, Logical disjunction; 15, true, Tautology.
Stroje a dobře vyškolení lidé používají tento look at table přístup k provádění základních závěrů, a ke kontrole, zda jiné závěry (pro stejné prostory) lze získat.
Uvažujme o následujících předpokladech: „Jestliže dnes prší, pak dnes na kánoi nepojedeme. Jestliže dnes nepojedeme na výlet na kánoi, pak zítra pojedeme na výlet na kánoi. Proto (Matematický symbol pro „proto“ je ), jestliže dnes prší, pojedeme zítra na výlet na kánoi.
Abychom využili pravidla odvození ve výše uvedené tabulce, necháme být výrok „Jestliže dnes prší“, bude „Dnes na kánoi nepojedeme“ a necháme být „Zítra pojedeme na výlet na kánoi“. Pak tento argument má formu:
Podívejme se na složitější soubor předpokladů: „Dnes není slunečno a je chladněji než včera“. „Půjdeme plavat, jen pokud je slunečno“, „Pokud nepůjdeme plavat, pak budeme mít grilování“, a „Pokud budeme mít grilování, pak budeme doma do západu slunce“ vést k závěru „Budeme doma před západem slunce.“
Důkaz podle pravidel inference: Nechť je tvrzení „Dnes je slunečno“, tvrzení „Je chladněji než včera“, tvrzení „Půjdeme plavat“, tvrzení „Budeme mít grilování“, a tvrzení „Budeme doma do západu slunce“. Pak se hypotézy stanou a . Pomocí naší intuice se domníváme, že závěr by mohl být . Pomocí tabulky Pravidla inference můžeme domněnku snadno doložit: