CADProof

CADproof will incorporate the techniques for managing heterogeneous reasoning pioneered in Hyperproof into a prototype design support tool. A greatly simplified and preliminary sketch of how this may be accomplished is illustrated in the next few pages.

Proof structure, represented in Hyperproof inside the main proof window, will be represented by a navigation palette, shown here on the left. Steps in the proof are represented by dots, with the subproof structure indicated by vertical lines. The step in focus (i.e., displayed and editable) is indicated by a solid dot; steps not currently in focus are indicated by hollow dots. Blue dots indicate open steps, those that have not been ruled out; red dots indicate closed steps. The proof structure is collapsible: a right-pointing triangle indicates a collapsed range of cases; a downward pointing triangle displays the contained cases.

Here, the overall proof contains two main cases, each of which has an embedded range of cases that are collapsed in the navigation palette. The step in focus is the "given" information, in this case the existing residence to which a guest suite is to be added.