Extended Armstrong's Axioms Proof Checker

Proof Format: (FD) (Reason)

• (FD) Format: {source} -> {target}
• Reasons:
1. [Given]: Assumptions, any FD can be accepted.
2. [Reflexivity]: {target} must be subset or equal to {source}
3. [Augmentation of (line) with {attr}]: where line is the referenced line and {attr} is the additional set of attributes
4. [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
5. [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