Heterogeneous Reasoning

When the project began it was concerned with the development of software tools for teaching logic. As this project progressed we became convinced that the subject matter of logic could, and should, be expanded to consider information that is not represented as sentences, as has historically been the case. This led us to develop a theory of heterogeneous reasoning, which is a major focus of the Openproof project.

The connection between our work in logic education and that in heterogeneous reasoning can be understood through our description of the evolution of the project. If you would like to read a 1996 paper by Barwise and Etchemendy explaining why they developed this software and how it has changed their view of logic, check out "Computers, Visualization, and the Nature of Reasoning."

Heterogeneous Reasoning

Formal logic, as traditionally conceived, concerns the process of reasoning only with information expressed as sentences of a formal language, thought of as formalizations of sentences expressed in writing or speech in a natural language.

This restricted view of logic has led to a well-developed theory of arguments presented in sentence form, but that theory is largely unable to model a large class of real-world reasoning problems. There are two related reasons. The first is that real-world reasoning often involves using information represented in non-sentential form, such as maps, spreadsheets, organization charts, Venn diagrams and photographs. The second is that such reasoning often involves information expressed in many such representations simultaneously. For example in order to find your way to a party in downtown San Francisco, you may utilise written information in the form of an address and/or directions, together with a street map and perhaps additionally a transit map showing the bus lines within the city. We refer to reasoning which simultaneously involves multiple representations of information as heterogeneous reasoning.

Our interest in heterogeneous reasoning stems in part from the development of the Tarski's World software, which we use in three of our courseware packages. Tarski's World can be used to explore the semantics of first-order logic by writing sentences in an interpreted language, and building worlds in which those sentences may be evaluated for truth. One type of exercise that can be done with the software takes the following form: open a collection of first order sentences, and a world. The sentences involve the use of names, denoting objects in the world, but the world does not have names for its objects (think of this as being at a cocktail party with people that you don't know, but prepared with information such as "Dave speaks with an English accent"). The exercise is to associate the names with objects in the world so that the sentences all come out true.

There is a clear criterion for successful reasoning here: one uses the information given to reason to the relevant conclusions, but such reasoning cannot be naturally modelled in first-order logic (the natural expression of the conclusion is a labelling of the world, not a first-order sentence, for example.)

Hyperproof

In the mid 80s, Jon Barwise and John Etchemendy developed a theory of heterogeneous reasoning. It was implemented as Hyperproof in the early 90s. The Hyperproof text book and software package combines graphical and text-based information, and presents a set of logical rules for integrating these different forms of information.

You can see a sample proof and read about the Hyperproof proof system here.

Hyperproof was developed as part of a courseware package in which we teach formal heterogeneous reasoning. However we believe that the techniques embodied in Hyperproof are generally applicable. Indeed, we believe that heterogeneity is a pervasive feature of everyday reasoning.

The Openbox

A major current focus of our research is the development of the Openbox. This phase of the research focuses on managing reasoning when dealing with information from many different sources, both graphic and text-based, and seeks to develop a structure to record decisions and the rationale behind them.

The Openbox generalizes Hyperproof along a number of different dimensions.

• The Openbox can support arbitrary representations, not just Hyperproof's blocks situations, and first-order logic.
• The Openbox will allow the construction of proofs involving arbitrarily many (one or more) distinct representations, rather than Hyperproof's two.
• The Openbox is implemented using a component architecture, so developers can implement their own representations, editors and inference systems and plug them into the Openbox architecture to quickly obtain reasoning environments for the representation.

Applications of the Openbox

Consider for example the task of planning the extension to a house. An architect or designer must consider a myriad of factors when designing a building: building codes, site constraints, aesthetic preferences, cost, to name a few. This type of reasoning might be modelled in an application which would allow designers to formalize their design reasoning in a logical, structured format. For the project clients, it could serve as a presentation tool as proof (or at least an argument) that a particular design (conclusion) is the best solution.

Look at a mockup of an application supporting this idea: CADProof.