A diagrammatic proof search procedure as part of a formal approach to problem solving.
Diderik Batens · 2006
This paper aims at describing a goal-directed and diagrammatic method for proof search. The method (and one of the logics obtained by it) is particularly interesting in the context of formal problem solving. A typical property is that it consists of attempts to justify so-called bottom boxes by means of premise elements (diagrammatic elements obtained from premises) and logical elements. Premises are not preprocessed, whence most premises lead to a variety of premise elements. The method is simple and insightful in three respects: (i) diagrams are constructed by drawing the goal node and superimposing the top node of a new diagrammatic element on a bottom box of an element that occurs in the diagram; (ii) diagrammatic elements are built up from binary and ternary relations that connect nodes (comprising one or two boxes) to boxes (entities containing a single formula); (iii) diagrammatic elements are obtained in view of existing bottom boxes by a unified approach. At