Automated Reasoning Project, Australian National University
This is a wide ranging and varied collection of papers. You might think that there is no common thread between them, except for the fact that they were all presented over the one weekend. However, that would be wrong. The papers form a coherent body of work, even though the participants come from widely different traditions.
1 Smart Logics
Four papers in the collection consider particular formal systems which are designed to closely model particular phenomena. Mortensen's paper argues for the usefulness of a paraconsistent logic in describing discontinuous phenomena, Schmidt and Chen's paper considers a formal system for reasoning about objects in the context of concurrent behaviour, and both Restall and Slaney's and Wobcke's papers consider ways of formalising belief revision. These are markedly different projects, but they all share the goal of shaping the logic to model the phenomenon under investigation. For example, the two belief revision papers argue for a modification of the standard postulates of belief revision to better model the real-life behaviour of belief revision. For Wobcke, the problem with standard belief revision is rational monotony. For Restall and Slaney, the problem is the postulate that belief sets be theories of classical logic. In finetuning the account of belief revision to take care of either of these problems, we more adequately account for the data.
So, these papers all consider what we like to call smart logics. That is, formal systems which pay close attention to the behaviour of what they're attempting to model. This way, they stay true to the phenomena, and in implementing them we will get a good fit to the problems being analysed. Typical examples of smart logics are those which handle inconsistencies sensibly (paraconsistent logics), those which take account of non-monotonicity and relevance (conditional logics, relevant logics, and others), and those which encode operators to deal with times, and other modal notions (temporal and modal logics). It is one thing to have formal systems which closely fit the phenomena. It is another to be able to implement them.
2 Smart Presentations
Four papers in the collection consider ways around this problem. For implementation of smart logics there are two different issues. Firstly, there is the problem of the number of logics to be implemented. If we have a different formal system for every application, then writing a theorem prover or some other kind of implementation for each system is going to be a tedious task. We would very much like to have a general framework for many different logics. Such a framework would be a smart presentation of a range of smart logics. One plausible `smart framework' is Nuel Belnap's Display Logic, and in their papers, Gor?e and Restall argue that this framework is a good one for studying the wide range of formal systems we're interested in pursuing.