2 months ago
- The Incredible Proof Machine is a visual tool for performing proofs in logics like propositional and predicate logic by dragging and connecting blocks.
- Users add blocks representing proof steps; if the conclusion turns green, a complete proof has been created.
- The tool aims to convey the fun of computer-aided proofs without requiring prior knowledge of syntax from theorem provers like Isabelle.
- Formula entry is limited to certain blocks (e.g., ¬-block) using abbreviations such as & for ∧, | for ∨, -> for →, ^ for ↑, ~ for ¬, ! for ∀, ? for ∃, and False for ⊥.
- Proofs are currently saved only in the browser's local storage and may be lost; future plans include server-side saving.
- The tool is free software, allowing contributions; for academic details, see related publications.