Armstrong's Axioms Proof Checker
Proof Format: (FD) (Reason)
- (FD) Format:
{source} -> {target}
- Reasons:
-
[Given]
: Assumptions, any FD can be accepted.
-
[Reflexivity]
: {target}
must be subset or equal to {source}
-
[Augmentation of (line) with {attr}]
: where line
is the referenced line and {attr}
is the additional set of attributes
-
[Transitivity of (line1) and (line2)]
: the following constraints must be satisfied
- Source at
line1
is equal to {source}
- Target at
line2
is equal to {target}
- Source at
line2
is equal to target at line1
-
[QED]
: {source} -> {target}
must be have been achieved
Buttons
- : Parse the proof
- : Step forward and check the next line on the proof
- : Step backward and undo one line of proof
- : Check until the end of the proof (or until error detected)
- : Undo all checks
Toggle
- : Show all derived hyperedges
- : Step only given hyperedges