LCS Publication Details
Publication Title: Combining diagrammatic and symbolic reasoning
Publication Author: Arkoudas, Konstantine
Additional Authors:
LCS Document Number: MIT-LCS-TR-1002
Publication Date: 10-6-2005
LCS Group: Program Analysis
Additional URL:
Abstract:
We introduce a domain-independent framework for heterogeneous natural deduction that combines diagrammatic and sentential reasoning. The framework is presented in the form of a family of denotational proof languages (DPLs). Diagrams are represented as possibly partial descriptions of finite system states. This allows us to deal with incomplete information, which we formalize by admitting sets as attribute values. We introduce a notion of attribute interpretations that enables us to interpret first-order signatures into such system states, and develop a formal semantic framework based on Kleene\'s strong three-valued logic. We extend the assumption-base semantics of DPLs to accodomodate 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. In addition, we specify detailed algorithms for implementing proof checkers for the resulting languages, and discuss associated efficiency issues.
To obtain this publication:

To purchase a printed copy of this publication please contact MIT Document Services.