Making the simple complicated is commonplace; making the complicated simple, awesomely simple, that's creativity. -- Charles Mingus

Monday, June 29, 2015

Heterogeneous Reasoning and the Openbox

We call reasoning that involves using multiple representations, heterogeneous.

It is a little odd that we have to qualify reasoning as heterogeneous, since this is the typical case.  When you are finding your way to a party at my house, you might combine my address (textual information) with a map (diagrammatic information) to decide on a route to take.  When you decide to take an umbrella after looking out of the window and  listening to the weather forecast,  you are likewise reasoning heterogeneously.  We do it all the time.

Conversely, homogeneous reasoning is pretty rare.  Mathematicians do it all the time, sure, but they aren't typical reasoners.  And of course you're asked to do it in most logic classes, which as we all know are excellent preparation for real life reasoning.

Anyway, one of the things that I am interested in is heterogeneous reasoning, and as part of the Openproof project, we have implemented the Openbox, which is a computational framework for exploring heterogeneous reasoning.

The idea behind Openbox is that it provides a representation-free proof environment.  It allows you to create proofs, adding steps, performing citation, saving and opening proof files, etc; but it contains no representations to put in the steps.  These have to be provided later.

Our application Fitch (part of the Language, Proof and Logic courseware package) is built in exactly this way.  When we add the first-order logic representation to the Openbox, we get a proof editor whose steps contain first-order sentences.  Of course, the representation comes with inference rules and tools for editing sentences, and so you obtain a rich application.

We are hoping to soon release Hyperproof, an application which allows you to build heterogeneous proofs involving first-order logic and blocks world diagrams similar to those used in Tarski's World (also part of Language, Proof and Logic, or available as part of the Tarski's World courseware package).  We build Hyperproof by adding both representations to the Openbox, and in addition adding a heterogeneous component that allows the two representations to work together.

At Diagrams 2014, we presented a program that we called HyperVenn which is a heterogeneous reasoning system for the previously mentioned blocks world diagrams together with Venn diagrams.

So in general, Openbox can be used to construct heterogeneous reasoning systems involving arbitrary, and arbitrarily many, representation systems.

No comments:

Post a Comment