In order to replicate the pen and paper experience of constructing a truth tree, we want to allow users to make more mistakes by requiring them to do each step of node decomposition manually, while preserving the existing node resolution functionality as an automatic mode.
As Carnap is both a proof assistant and a tool for teaching logic, our interface design must reconcile conflicting goals. As a proof assistant, it should prevent the user from making mistakes where possible, and provide as much assistance as it can. As a teaching tool, it is appropriate to allow mistakes, and limit how much assistance the widget gives the student. Adding configuration options should help resolve the tension between these goals.
Notes on discussion, these should each be addressed and possibly converted to issues before closing this issue:
In auto mode, it is easy enough to allow a user to undo the closing of a branch and keep the tree correct. We can just allow phantom nodes to continue being created under the "closed" node.
The behaviour for auto mode of appending to all open branches may not make sense in first order case.
In manual mode, a user should have to do all of the following manually. For now, our design philosophy for manual mode will be "keep all mistakes possible.":
Mark a node as resolved.
Append each new branch or pair of branches manually.
Fill in the formulas for each new node manually. This means it makes sense to create node as initially blank.
We may need to consider the possibility that a student could cheat by inspecting the javascript and switching the mode to auto. However, if a student wants to cheat, they could simply use another tool to construct the whole tree automatically.
From our video call discussion on August 2nd:
In order to replicate the pen and paper experience of constructing a truth tree, we want to allow users to make more mistakes by requiring them to do each step of node decomposition manually, while preserving the existing node resolution functionality as an automatic mode.
As Carnap is both a proof assistant and a tool for teaching logic, our interface design must reconcile conflicting goals. As a proof assistant, it should prevent the user from making mistakes where possible, and provide as much assistance as it can. As a teaching tool, it is appropriate to allow mistakes, and limit how much assistance the widget gives the student. Adding configuration options should help resolve the tension between these goals.
Notes on discussion, these should each be addressed and possibly converted to issues before closing this issue: