| 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.
|