Highlights

Automated Reasoning Project

Honours and Awards

Automated Reasoning Project

Dr Rajeev Goré
Awarded an Australian Research Council QEII Fellowship (5 years from July 1997)

Professor Robert Meyer
Awarded a University Fellowship

Staff and Students

Automated Reasoning Project

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)

Research

Automated Reasoning Project

Introduction

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:

Decision Problems and Optimisation

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.

Display Calculi


Researchers: Dr Jeremy Dawson, Dr Rajeev Goré
External Researchers: Professor Nuel Belnap (University of Pittsburgh, Pittsburgh Campus, USA), Dr Marcus Kracht (Free University Berlin, Berlin, Germany), Dr Gregory Restall (Macquarie University, Sydney), Dr Heinrich Wansing (University of Leipzig, Leipzig, Germany), Dr Stéphane Demri, (LIFIA - CNRS, Grenoble, France)

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.

Intensional Logics

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.

Semantically Guided Theorem Proving

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.

Substructural Logics

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.

Automated Deduction on Smart Cards

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.

Research Dissemination

Publications

Automated Reasoning Project

Books

G. Antoniou*, J.K. Slaney# (Eds)
Proceedings of Australian Joint Conference on Artificial Intelligence (AI98), Springer Verlag, Berlin (1998)

Book Chapters

J. Denzinger*, M. Fuchs#
'A Comparison of Equational Reasoning Heuristics', in Automated Deduction. A Basis for Applications, W. Bibel, P.H. Schmitt (Eds), Kluwer Academic Publishers, 361-382 (1998)

Refereed Journal Publications

M. Fuchs$, M. Fuchs#
'Feature-based Learning of Search-guiding Heuristics for Theorem Proving', AI Communications, ??? ???-??? (1998)

R. Goré#
'Substructural Logics on Display', Logic Journal of the Interest Group in Pure and Applied Logic, 6(3) 451-504 (1998)

R. Goré#
'Gaggles, Gentzen and Galois: How to display your favourite substructural logic', Logic Journal of the Interest Group in Pure and Applied Logic, 6(5) 669-694 (1998)

T. Surendonk+
'On Isomorphisms Between Canonical Frames', Advances in Modal Logic, Marcus Kracht, Maarten de Rijke, Heinrich Wansing, Michael Zakharyachev (Eds) 1 249-269 (1998)

Refereed Conference Publications

B. Beckert$, R. Goré#
'System Description: LeanK 2.0: Free Variable Tableaux for Propositional Modal Logics: Decision Procedures', Proceedings of the International Conference on Automated Deduction, Lindau, Germany, 51-55, 5-10 July 1998

N. Bonnette%, R. Goré#
'A Labelled Sequent System for Tense Logic Kt', Proceedings of the 11th Australian Joint Conference on Artificial Intelligence (AI98), Brisbane, 71-82, 15-17 July 1998

J. Dawson+, R. Goré#
'A Mechanised Proof System for Relation Algebra using Display Logic', Proceedings of the European Workshop on Logic in Artificial Intelligence, Daghstul, Germany, 264-278, 12-15 October 1998

J. Dawson+, R. Goré#
'A Mechanisation of Classical Tense Display Logic', Proceedings of the 11th Australian Joint Conference on Artificial Intelligence (AI98), Brisbane, Australia, 107-118, 15-17 July 1998

S. Demri$, R. Goré#
'An O n.log n3-time transformation of Grz into decidable fragments of classical first-order logic', Proceedings of the International Workshop on First-Order Theorem Proving, Schloss Wilhelminenberg, Vienna, Austria, 127-134, 23-25 November 1998

M. Fuchs#
'Crossover versus Mutation: An Empirical and Theoretical Case Study', Proceedings of the 3rd Annual Conference on Genetic Programming (GP-98), Wisconsin, USA , 78-85, 22-25 July 1998

M. Fuchs#
'A Feature-based Learning Method for Theorem Proving', Proceedings of the 15th National Conference on Artificial Intelligence (AAAI-98), Wisconsin, USA , 457-462, 26-30 July 1998

R. Goré#, J. Posegga$, A. Slater%, H. Vogt$
'System Description: cardTAP - the first deduction on a smart card', Proceedings of the 15th International Conference on Automated Deduction (CADE-15), Lindau, Germany , 47-50, 5-10 July 1998

J. Slaney#, S. Thiébaux*
'On the Hardness of Decision and Optimisation Problems', Proceedings of the European Conference on Artificial Intelligence (ECAI 98), Brighton, United Kingdom, 244-248, 23-28 August 1998

A. Slater%, R. Goré#, J. Posegga$, H. Vogt$
'cardTAP: Automated Theorem Proving on a Smart Card', Proceedings of the 11th Australian Joint Conference on Artificial Intelligence (AI98), Brisbane, Australia, 239-248, 15-17 July 1998

H. Wang%
'Constraint Resolution Within Object Hierarchies', Proceedings of the 11th Australian Joint Conference on Artificial Intelligence (AI98), Brisbane, Australia, 180, 15-17, July 1998

H. Wang%, J.K. Slaney#
'Towards Knowledge Encapsulation', Proceedings of the 21st Australasian Computer Science Conference, Perth, Australia , 193-204, 4-6 February 1998

H. Wang%, J.K. Slaney#
'The Design of an Intelligent System for Retrieving and Compiling Information Over the World Wide Web', Proceedings of the 1st Asian Pacific Web Conference (APWeb98), Beijing, China , 319-324, 27-30 September 1998

H. Wang%, J.K. Slaney#
'Distributed Scheduling within Constrained Object Hierarchies', Proceedings of the International Symposium on Operations Research and its Applications (ISORA'98), Kunming, China, 29-38, 20-22 August 1998

H. Wang%, J.K. Slaney#
'GISM: A Language for Modelling and Developing Agent-based Intelligent Systems', Proceedings of the Fourth Australian Workshop on Distributed Artificial Intelligence, Brisbane, Australia, 139-153, 15-17 July 1998

Other Publications

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