- Professor Meyer, who retired last year, was awarded a University Fellowship in November. This Fellowship is awarded to honour an exceptionally distinguished person and to enable that person to work in the University after retirement.
- A Memorandum of Understanding was signed this in March of this year with Instituto per la Ricerca Scientifica e Tecnologica (IRST) of Trento, Italy. Dr John Slaney visited Trento for 3 days in August to discuss research projects of mutual interest.
- Dr Rajeev Goré was promoted to Fellow in July.
- Tim Surendonk was awarded his PhD degree in September.
- Phan Hong Giang completed his Master of Science degree in February.
- With colleagues from Deutsche Telekom, Rajeev Goré and Andrew Slater successfully implemented the first theorem prover to run on a smart card.
- Dr Stéphane Demri (Leibniz Laboratory, Institute Informatique Mathématiques Appliquées Grenoble - Centre National De La Recherche Scientifique, Grenoble, France) spent six months with the Automated Reasoning Project as an ARC International Fellow. This gave an important boost to our work on display logics and modal logics.
- The sixth annual Logic Summer School held in January was again a great success. Selected students from Australia and New Zealand enjoyed two weeks of introduction to many aspects of logic. This year, presenters came from Japan, France and Germany, as well as from Australia.

**Dr Rajeev Goré**

Awarded an Australian Research Council QEII Fellowship (5 years from July 1997)

**Professor Robert Meyer**

Awarded a University Fellowship

**Senior Fellow and Head**

http://arp.anu.edu.au/~jks/

John K. Slaney, MA *Cambridge*, PhD *ANU*

**Fellow**

http://arp.anu.edu.au/~rpg/

Rajeev P. Goré, BSc MSc *Melbourne*, PhD *Cambridge*
(Half time)

**Research Fellow**

http://arp.anu.edu.au/~fuchs/

Matthias Fuchs, Diplom, MSc PhD
*Kaiserslautern* (!!! What is this (Diplom) = Similar to our BSc !!!)

**Postdoctoral Fellow**

http://arp.anu.edu.au:80/~jeremy/

Jeremy Dawson, BSc MSc *Sydney*, PhD *Sheffield*
(Quarter time)

**Department Administrator**

mailto:catrina.waterson@anu.edu.au

Catrina Waterson (Half time)

**Technical Assistance**

mailto:joe.elso@anu.edu.au

Joe Elso, BSc Grad. Dip. Comp. Sci. *Canberra* (Half time)

**University Visiting Fellows**

Dr Stéphane Demri (Institute Informatique
Mathématiques Appliquées Grenoble - Centre National De La
Recherche Scientifique), Grenoble, France) (ARC International Fellow)

Emeritus Professor Robert K. Meyer (ANU)

Professor Torsten H. Schaub (Universität Potsdam, Potsdam, Germany)

Dr Timothy J. Surendonk (ANU)

**Short Term Visitors**

Dr Ryo Kashima (Japan Advanced Institute of Science and Technology, Japan)

Professor Storrs McCall (McGill University, Montreal, Canada)

Professor Hiroakira Ono (Japan Advanced Institute of Science and
Technology, Japan)

Dr Maurice Pagnucco (University of New South Wales, Sydney)

Dr Joachim Posegga (Deutsche Telekom AG, Germany)

Dr Nobu-yuki Suzuki (Shizuoka University, Shizuoka, Japan)

**Graduated Students**

http://arp.anu.edu.au:80/~giang/

Hong Giang Phan, Dip. Inf. Proc. *Russia*, enrolled February 1996,
AUSAID Scholarship

http://arp.anu.edu.au:80/~tsurend/

Timothy Surendonk, BSc *Auckland*, MA *UCLA*, enrolled
January 1995, CSFP Scholarship

**PhD Students**

http://arp.anu.edu.au:80/~nic/

Nicolette Bonnette, BSc *Victoria*, enrolled January 1998, ANU
Scholarship

http://arp.anu.edu.au:80/~duc/

Ngoc Duc Ho, Magister Artium, Diplom-Informatiker *Leipzig*,
enrolled July 1996, OPRS Scholarship

http://arp.anu.edu.au:80/~kahlil/

Kahlil Hodgson, BSc MSc *Auckland*, enrolled March 1997, ANU
Scholarship

http://arp.anu.edu.au:80/~andrews/

Andrew Slater, BSc *ANU*, enrolled June 1997, ANU Scholarship

http://arp.anu.edu.au:80/~wongas/

Paul Wong, BA MA *Canada*, enrolled August 1997, OPRS Scholarship

http://cs.anu.edu.au/people/Hongxue.Wang/

Hongxue Wang, BSc MSc *China*, enrolled June 1995, ADCOS
Sholarhsip (PhD Student in Computer Science, FEIT,
co-supervised by Dr John Slaney)

**Masters Students**

Hong Giang Phan, Dip. Inf. Proc., *Russia* (until February)

**Summer Scholars**

Francis Hawcroft (University of Auckland)

Reasoning is the process of drawing conclusions from information. As computers become more powerful, their ability to perform complicated reasoning tasks increases. In order to harness their power, we need to understand the reasoning they do and how they may do it more efficiently. This investigation begins with logic. A system of logic is a mathematical theory aimed at defining which inferences are the valid ones.

One system that is well understood is classical first order logic: the logic you get by assuming that every sentence has a precise value (it is 'true' or 'false') and by confining attention to the expressions 'and', 'not', 'all' and what can be defined in terms of those. Classical logic is surprisingly rich and expressive, but like many all-purpose instruments it tends to be cumbersome, so it is important to study alternatives to it and extensions of it, known collectively as non-classical systems.

The research of the Automated Reasoning Project has two main aspects:

- We investigate the mathematical properties of non-classical logics. For example, we want to know what happens if sentences are evaluated on a sliding scale between 'true' and 'false' rather than just using the two absolute values. We are also interested in what sort of logic is useful for reasoning about time and change, in logics designed to handle incomplete and inconsistent information and in logics with built-in mechanisms for keeping track of resources as events take place.
- We study algorithms for reasoning in various systems, both classical and non-classical. We wish to observe how these algorithms behave, for its intrinsic interest and with a view to practical applications. One type of program is for proving that a conclusion follows from given information. A different type of reasoning program generates models of the information. That is, it searches for interpretations of the given information, showing how things might be if that information were true. One of our interests is in combining model generation with theorem proving so that the two kinds of reasoning can interact. This leads to programs which can search more intelligently, and therefore more efficiently, for solutions to problems.

*Researcher:* Dr John Slaney
*External Researcher:* Dr Sylvie Thiébaux (INRIA, France
and CSIRO, Australia)

Many problems take the form of a search for the 'smallest' solution. For instance, a transport company wants a truck to visit a list of places, keeping the total distance covered to a minimum, and so the company wants to know in which order to make the visits. Computing the optimal order is too hard to be feasible, so we are interested in efficient ways of finding 'good' if suboptimal solutions. One approach is to ask whether there exists a solution better than some limit. For instance, rather than worrying about whether the perfect journey for the truck is 94.5 or 94.6 km, the company may only care whether there is some solution that makes the total journey less than 100 km. This version of the problem calls for a decision (is there such a journey or not?) rather than for optimisation.

If we know the size of the problem (how many places to visit, for example) we can estimate how hard it will be to find the optimal solution. If we know how far apart the places are on average, we can also estimate how hard it will be to answer the decision problem with a given decision threshold. It turns out that estimating the average hardness of decisions is of little use for predicting how hard the optimisation will be. However, we do know that for any particular case (eg. a particular set of places), there is simple formula relating the hardness of decisions with various decision thresholds to the optimal value and to the difficulty of proving its optimality. In work reported this year, we have studied the predicted hardness of decisions given the estimated hardness of optimisation. Currently we are investigating the converse idea of observing the actual (rather than estimated) hardness of decision problems to make predictions about optimisation.

Recently, a new type of proof system called Display Calculi have begun to gain attention. Like many other proof systems, display calculi build up valid forms of reasoning by putting together simpler ones, so that in order to search for a proof of a particular formula, it is only necessary to decide whether certain strictly simpler formulae are provable. Display Calculi are designed to handle many different nonclassical logics, on their own or in combination. The name comes from a fundamental property of the system that allows any particular constituent of a structure to be chosen and 'displayed' by moving all of the other constituents over to the other side of the equation or 'sequent'.

The advantage of special purpose 'smart' logics is that they are closely related to their application domains, building in useful features: for example, temporal logics build in properties like the direction of time, the semantics of 'next' and 'until' and so forth. The advantage of general purpose logics, on the other hand, is that their proof theory and model theory are uniform and fairly well understood. Display Calculi are one attempt to find a middle way, keeping as far as possible the desirable features of both kinds of system. It offers a way of doing logic that is modular and widely applicable.

Given the broad applicability of display calculi, there is a need to characterise the class of logics that can be handled within this new framework. We are investigating the expressive power of display calculi by concentrating on propositional modal logics. An important property for propositional modal logics is whether or not they form a subset of classical first-order logic. We have already found a display calculus for the modal logic G, which is known to be outside first-order classical logic, and are extending this to other such logics like Grz and S4.3.1. However, somewhat paradoxically, we have also discovered an efficent translation of Grz into a decidable fragment of classical first-order logic, which allows us to use traditional theorem provers for classical first-order logic to find proofs in Grz. On another track, we have found display calculi for a large class of logics with applications in Artificial Intelligence.

In related research, we are implementing Display Logic using a general interactive theorem proving framework called Isabelle. By instantiating this implementatiuon in a rigorous and disciplined way, users will be able to build interactive theorem provers for particular hybrid nonclassical logics to suit their needs.

*Researchers:* Dr Rajeev Goré, Dr Timothy Surendonk, Mr Ho
Ngoc Duc, Ms Nicolette Bonnette
*External Researchers:* Dr Bernhard Beckert (University of
Karlsruhe, Karlsruhe, Germany)

To interpret the language of classical logic we assign a value to each proposition, saying whether it is true or false. An important extension of this idea is to combine a whole set of interpretations into one, so that each proposition simultaneously gets a set of values. In order for this to produce the required logical systems, these valuations must be related to each other in some way. Different kinds of relation produce different non-classical logics.

For example, the set of valuations may represent the successive states of
affairs at a series of different times. This enables us to model propositions
involving the future tense (about what **will** be the case) or the past
tense
(what **was** the case). Hence we can handle reasoning about events, changes
over time and the possible states of dynamic systems such as computers
executing a program or investors reacting to stock prices.

Many nonclassical logics can be modelled using valuation points
connected by binary relations. By explicitly naming these points and
manipulating formulae of the form *w:A* (meaning that point *w*
makes formula *A* true), it is possible to give deductive calculi
for these logics. A natural way to formulate such calculi is as semantic
tableaux, in which each assignment of a value to a labelled formula is
recursively analysed into simpler components.

Modal logics allow greater expressiveness than classical logic by
allowing operators which capture notions like 'statement *S* is
true at all future times', 'statement *S* was true at some past
time', or even 'agent *A* believes that statement *S* will
become true in some future time'. But most current programs for
automated deduction using these logics are huge. By tailoring our
theoretical calculi to mimic operations from the programming language
Prolog, we have shown that efficient automated deduction in these logics
can be carried out using programs of fewer than 50 Prolog lines. Such
'lean' programs are not only easy to verify, but also are easy to embed
in more complicated systems which are themselves under development.

*Researchers:* Mr Kahlil Hodgson, Dr John Slaney

Most computer programs for generating logical proofs search in a fairly undirected fashion. This is because they deal only with one formula at a time, asking whether a specific move can be applied (eg. whether an equation can be simplified). In many practical systems, these searches take an unduly long time, so more efficient methods are sought.

Our system SCOTT is an attempt to inject more intelligence into the search, by giving a theorem prover some rudimentary understanding of the problem it is addressing. We are currently working on ways to extract more information about the meaning of problems by computing several interpretations in parallel, rather than just one. There is a trade-off between time spent looking for these interpretations and the efficiency resulting from a more focused search.

Our experiments indicate that there are interesting effects, especially when multiple models are being used, but the impact on proof searches is hard to predict. We are now analysing some thousands of proofs statistically to discover what semantic features are most relevant to them.

*Researchers:* Professor Robert Meyer, Dr John Slaney
*External Researchers:* Professor Michael Dunn (Indiana
University, Bloomington Campus, USA), Dr Gregory Restall
(Macquarie University, Sydney)

Some logical rules are concerned with the meaning of expressions involving 'all', 'some', 'and' or 'if'. However, there are other principles of reasoning called structural rules. These have to do with the way arguments can be manipulated in general. For instance, the rule of 'exchange' states that the order in which assumptions are made is irrelevant to the validity or invalidity of conclusions drawn from them. Another structural rule is 'contraction.' It says that assumptions made in the course of an argument can be used as often as we like without having to be re-assumed. Substructural logic is the study of reasoning systems obtained by holding the logical rules constant but changing the structural rules, in such a way that the meaning of expressions does not vary.

The benefits of this approach may be illustrated with 'linear logic', a well known substructural system. Exchange is allowed, but contraction is not. If we think of the assumptions of an argument as 'resources' which get consumed when they are used in inferences, we may apply linear logic rather naturally to problems of reasoning about processes, in which successive actions cost resources and in which each resource may only be spent once. A closely related system is 'relevant logic'. This permits contraction, so each resource may be used multiple times. However, unused resources are tracked by not allowing irrelevant assumptions to be discarded.

The ARP's tradition of work on substructural logics continued in 1998. It was shown that arithmetic based on linear logic allows no linear implications between numerical equations other than the trivial ones corresponding to the operation of adding or subtracting a term from each side of the equation. This implies that certain techniques for embedding ordinary classical arithmetic in theories based on relevant logic will not work when the underlying system is weakened by dropping contraction.

*Researchers:* Dr Rajeev Goré, Mr Andrew Slater
*External Researchers:* Mr Joachim Posegga and
Mr Harald Vogt (Deutsche Telekom, Germany)

Very soon, a credit-card sized card with an on-board computer will amalgamate its owner's credit card, phone card, welfare card, library card, and licence card into one single 'smart card' containing an electronic purse and other personal information. An owner will download special applications off the Internet that run on the on-board computer by inserting the card into an automatic teller machine. Given the highly personal information stored on the card, one method for vouching for the safety of downloaded code is for such code to carry a proof certifying its safety in some previously agreed (mathematical) logic. Smart cards will therefore need to check that complex proofs are correct using mathematical logic. Our prototype implementation of a theorem prover has successfully run on a smart card, not only allowing us to check such proofs, but also allowing us to search for proofs using the card's on-board computer.

**G. Antoniou ^{*}, J.K. Slaney^{#}** (Eds)

**J. Denzinger ^{*}, M. Fuchs^{#}**

'A Comparison of Equational Reasoning Heuristics', in

**M. Fuchs ^{$}, M. Fuchs^{#}**

'Feature-based Learning of Search-guiding Heuristics for Theorem Proving',

** R. Goré ^{#}**

'Substructural Logics on Display',

**R. Goré ^{#}**

'Gaggles, Gentzen and Galois: How to display your favourite substructural logic',

**T. Surendonk ^{+}**

'On Isomorphisms Between Canonical Frames',

**B. Beckert ^{$}, R. Goré^{#}**

'System Description: LeanK 2.0: Free Variable Tableaux for Propositional Modal Logics: Decision Procedures',

**N. Bonnette ^{%}, R. Goré^{#}**

'A Labelled Sequent System for Tense Logic Kt',

**J. Dawson ^{+}, R. Goré^{#}**

'A Mechanised Proof System for Relation Algebra using Display Logic',

**J. Dawson ^{+}, R. Goré^{#}**

'A Mechanisation of Classical Tense Display Logic',

**S. Demri ^{$}, R. Goré^{#}**

'An O n.log n

**M. Fuchs ^{#}**

'Crossover versus Mutation: An Empirical and Theoretical Case Study',

**M. Fuchs ^{#}**

'A Feature-based Learning Method for Theorem Proving',

**R. Goré ^{#}, J. Posegga^{$}, A.
Slater^{%}, H. Vogt^{$}**

'System Description: cardTAP - the first deduction on a smart card',

**J. Slaney ^{#}, S. Thiébaux^{*}**

'On the Hardness of Decision and Optimisation Problems',

**A. Slater ^{%}, R. Goré^{#}, J.
Posegga^{$}, H. Vogt^{$}**

'cardTAP: Automated Theorem Proving on a Smart Card',

**H. Wang ^{%}**

'Constraint Resolution Within Object Hierarchies',

**H. Wang ^{%}, J.K. Slaney^{#}**

'Towards Knowledge Encapsulation',

**H. Wang ^{%}, J.K. Slaney^{#}**

'The Design of an Intelligent System for Retrieving and Compiling Information Over the World Wide Web',

**H. Wang ^{%}, J.K. Slaney^{#}**

'Distributed Scheduling within Constrained Object Hierarchies',

**H. Wang ^{%}, J.K. Slaney^{#}**

'GISM: A Language for Modelling and Developing Agent-based Intelligent Systems',

**N. Bonnette ^{%}, R.P. Goré^{#}**

'A Labelled Sequent System for Tense Logic Kt', Technical Report, TR-ARP-01-1998, Automated Reasoning Project, ANU, March 1998

**S. Demri ^{$}, R.P. Goré^{#}**

'Display Calculi for Logics with Relative Accessibility Relations', Technical Report, TR-ARP-04-1998, ANU, Australian National University, October 1998

**S. Demri ^{$}, R.P. Goré^{#}**

'Cut-free Display Calculi for Nominal Tense Logics', Technical Report, TR-ARP-07-1998, Automated Reasoning Project, ANU, June 1998

**M. Fuchs ^{#}**

'Automatic Selection of Search-guiding Heuristics for Theorem Proving', Technical Report, TR-ARP-02-1998, Automated Reasoning Project, ANU, April 1998

**M. Fuchs ^{#}**

'Finding Simpler Proofs in Logic Calculi', Technical Report, TR-ARP-08-98, Automated Reasoning Project, ANU, July 1998

**M. Fuchs ^{#}**

'A Data Mining Approach to Support the Creation of Loop Invariants Using Genetic Programming', Technical Report, TR-ARP-09-98, ANU, October 1998

**J. K. Slaney ^{#}, K. Hodgon^{%}**

'System Description: MScott', Technical Report, TR-ARP-06-98, Automated Reasoning Project, ANU, June 1998

**H. Wang ^{%}, J. Slaney^{#}**

'On Generalities of Intelligent Systems', Technical Report TR-ARP-05-98, Automated Reasoning Project, ANU, May 1998

**P. Wong ^{%}**

'From Weak Satisfiability to n-Satisfiability on Hypergraphs', Technical Report TR-ARP-10-98, Automated Reasoning Project, ANU, October 1998