Prove-It
Prove-It copied to clipboard
Implement Modus Ponens Proof Step Checker
The broader development/enhancement issue, of course, is the implementation of an independent general proof checker within the Prove-It system that would deal with all possible types of proof steps and rely on a relatively small (and thus easy -- or easier -- to check) block of code. We can begin, however, with the relatively simple but non-trivial Modus Ponens proof steps as a “demonstration of concept.” Immediate development tasks consist of: (1) deciding exactly where in the extant code to perform such a check; (2) where to “house” the checker code itself; and (3) where to “house” the resulting “check.” For example, concerning item (3), is it possible we might augment the Judgment class to hold a “Checked” object in addition to the expression, assumptions, and proof? And what might a “Checked” object look like? Perhaps “checked” just becomes a Boolean attribute of a Judgment?