A Framework Combining Diagrammatic and Symbolic Problem Solving
Konstantine Arkoudas, Selmer Bringsjord · 2007
We introduce Vivid, a domain-independent framework for mechanized heterogeneous natural deduction that combines diagrammatic and symbolic reasoning. The framework is presented in the form of a family of denotational proof languages (DPLs). We present novel formal structures, called named system states, that are specifically designed for modeling potentially underdetermined diagrams. These structures allow us to deal with incomplete information, which is a pervasive feature of heterogeneous problem solving. We introduce a notion of attribute interpretations that enables us to interpret first-order signatures into named system states, and develop a formal semantic framework based on a three-valued logic. We extend the assumption-base semantics of DPLs to accommodate diagrammatic reasoning by introducing general inference mechanisms for the valid extraction of information from diagrams and for the incorporation of sentential information into diagrams. A rigorous big-step operational semantics is given, on the basis of which we prove that our framework is sound. We present examples of particular instances of Vivid, and discuss related work.