List of Fragments = Proof Steps
A proof is a sequence of proof steps. The decomposition into fragments is the first phase for implementing proofs into an electronic environment. The following table shows the principles of the decomposition of a proof. Every step is a question in the e-proof environment, that is filled with context dependently with optional proof steps. You can create an e-proof with the iMathAS-Creator,
Step ID | Connection | Proof Step Description | Justification (Reason) |
Q1 | Precondition | Description of Proof Step 1: Let V be a vector space with ... | --- |
Q2 | => | Description of Proof Step 2 ... | Justification [J1],[J2] |
Q3 | => | Description of Proof Step 3 ... | Justification [J3],[J4],[J5] |
Q4 | => | (a+b)2 | --- |
Q5 | = | a2 + 2ab + b2 | Binomial Law |
... | ... | ... | ... |
Q8 | => | Description of Proof Step 8 ... | Justification [J6],[J7] |
Q9 | q.e.d | Theorem proved | ... |
e-Proof-Decomposition into Fragments
All proof steps in an e-proof can be decomposed into three Elements. The decomposition works as follows:
- (A) Proof decomposition into fragments: an e-proof is decomposed into single steps (fragments).
- (B) Fragment decomposition into three components: a single proof step (fragment) is decomposed into:
- (B1) connection to previous step,
- (B2) proof step description and
- (B3) the justification of the single proof step.
- (B1) connection to previous step,
- (C) Connection to previous proof step: a connection to the previous proof could be e.g.
- "=>" an implication derived from the previous proof step or
- "<=>" an equivalence to the previous proof step or
- "=" an equation, if the previous and the current proof step are algebraic terms.
Examples
The examples show, how a proof can be decomposed into three components in