mirror of
https://github.com/janishutz/eth-summaries.git
synced 2026-03-14 17:00:05 +01:00
9 lines
526 B
TeX
9 lines
526 B
TeX
\subsection{Natural deduction}
|
|
The rules from above here are used to construct derivations under assumptions, e.g.
|
|
$A_1, \ldots, A_n \vdash A$, which is read as ``$A$ follows from $A_1, \ldots, A_n$''.
|
|
|
|
The derivations are always represented as derivation trees and a \bi{proof} is a derivation whose root has no assumptions.
|
|
|
|
Since we have to prove a statement, we have to draw the derivation trees from the bottom up, with the goal of reaching an axiom or a rule that is an assumption
|
|
using the other rules of the rule set.
|