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