TR-ARP-01-94
John Slaney
The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure.
13 pages
This is an invited talk presented to CADE in Nancy (France) in June 1994. It
is noted that increasing reliance on computation is causing disquiet in the
field of finite mathematics. Recent research in the theory of quasigroups is
examined as an example. The conceptual issues concerning essentially computer-
generated proofs are examined, and it is suggested that Automated Reasoning
research especially in proof checking offers the best chance for alleviation
of the difficulties.
-------------------------------------------------------------------------------
TR-ARP-02-94
John Slaney
FINDER: Finite Domain Enumerator. System Description.
4 pages
This is the announcement of FINDER 3.0 from the Proceedings of CADE-12. It
contains a brief description and two examples to illustrate FINDER input. For
more information, see the Notes and Guide supplied with the program sources.
-------------------------------------------------------------------------------
TR-ARP-03-94
John Slaney, William McCune and Ewing Lusk
SCOTT: Semantically Constrained OTTER. System Description.
5 pages
This is the announcement of SCOTT 1.0 from the Proceedings of CADE-12. SCOTT
combines OTTER and FINDER into a new theorem prover.
-------------------------------------------------------------------------------
TR-ARP-04-94
John Slaney
Finite Models for some Substructural Logics
18 pages
This is a revised and updated version of TR-ARP-2/90 which was a paper
delivered to the Annual Conference of the Australasian Association for Logic
in Sydney in 1991 but was never published except as a technical report.
This paper is a report of computer-driven research into the modelling of
propositional systems related both to linear logic and to relevant logic.
One result is an exponential lower bound on the number of models of given
size validating such systems. Another theorem explores dualities within
models for such systems in order to explain striking regularities in the
distribution of models of the system C. In these researches the computer
figures not as a prover of theorems, nor even as a proof assistant, but as a
source of quasi-empirical data.
-------------------------------------------------------------------------------
TR-ARP-05-94
Greg Restall
Modalities in Substructural Logics
9 pages
This paper generalises Girard's results which embed intuitionistic logic
into linear logic by showinf how arbitrary substructural logics can be
embedded into weaker substructural logics, using a single mnodality
which `encodes' the new structural rules.
-------------------------------------------------------------------------------
TR-ARP-06-94
Greg Restall
Arithmetic and Truth in Lukasiewicz's Infinitely Valued Logic
8 pages
Peano arithmetic formulated in Lukasiewicz's infinitely valued logic
collapses into classical Peano arithmetic. However, not all additions
to the language need also be classical. The way is open for the addition
of a real truth predicate satisfying the T-scheme, into the language.
However, such an addition is not pleasing. The resulting theory is
omega-inconsistent. This paper consists of the proofs and interpretations
of these two results.
-------------------------------------------------------------------------------
TR-ARP-07-94
Adventures in Blocks World
John Slaney and Sylvie Thiebaux
31 pages
Despite over 25 years of its use as as the standard example in planning,
Blocks World (BW) is still little understood from a mathematical point of
view. Here we report a series of investigations of this surprisingly
complex structure, issuing in:
* simple expressions for the number of BW states and some theorems
concerning the numbers of states and partial states.
* a proof that it is easy to generate BW states using exhaustive
satisfiability techniques such as Davis-Putnam.
* a new polynomial time algorithm for near-optimal BW planning and some
notes on its behaviour.
* some observations concerning the average numbers of blocks that must
be moved in solving BW planning problems and the probability that all
blocks must be moved.
We close with an experimental comparison between our new algorithm and
certain others suggested in the recent literature. All of these
algorithms have the property of being `near-optimal' in the sense that
for some constant k they guarantee plans no longer than k times the
minimum possible.
-------------------------------------------------------------------------------
TR-ARP-08-94
Logical Laws
Greg Restall
9 pages
This paper is an introductory essay on the notion of a ``Logical Law.''
In it, I show that there are three important different questions one can
ask about logical laws. Firstly, what it *means* to be a logical
law. Secondly, what *makes* something a logical law, and thirdly,
what *are* the logical laws. Each of these questions are answered
differently by different people. I sketch the important differences in
views, and point the way ahead for logical research. (This paper is to
appear in Routledge's forthcoming Encyclopedia of Philosophy.)
-------------------------------------------------------------------------------
TR-ARP-09-94
Four-Valued Semantics for Relevant Logics (and some of their rivals)
Greg Restall
18 pages
This paper gives an outline of three different approaches to the four-valued
semantics for relevant logics (and other non-classical logics in their
vicinity). The first approach borrows from the `Australian Plan'
semantics, which uses a unary operator * for the evaluation of
negation. This approach can model anything that the two-valued account
can, but at the cost of relying on insights from the Australian
Plan. The second approach is natural, well motivated, independent of
the Australian Plan, and it provides a semantics for the contraction-free
relevant logic C (or RW). Unfortunately, its approach seems to
model little else. The third approach seems to capture a wide range of
formal systems, but at the time of writing, lacks a completeness proof.
-------------------------------------------------------------------------------
TR-ARP-10-94
Truthmakers, Entailment and Necessity
Greg Restall
11 pages
Australian Realist analytic philosophy is full of claims about truthmakers
and truthmaking. In this paper, I seek to show that a number of
intuitions about truthmaking are jointly inconsistent, and that some
common attempts at resolving the inconsistency are unsatisfying.
Finally, I propose an account of truthmaking which resolves the tensions
as best as possible. This account has great affinities with both relevant
entailment and situation semantics. This note can be seen as an
apologetic for relevant entailment for those who are familiar with
truthmaking, or as an introduction to truthmaking for those familiar
with logic. Either way, it is an attempt to apply modern logical methods
and insights to a philosophical problem.
-------------------------------------------------------------------------------
TR-ARP-11-94
Displaying and Deciding Substructural Logics 1: Logics with Contraposition
Greg Restall
41 pages
Many logics in the relevant family can be given a proof theory in the
style of Belnap's display logic. However, as originally given, the
proof theory is essentially *more expressive* than the logics they
seek to model. In this paper, we consider a modified proof theory
which more closely models relevant logics. In addition, we use this
proof theory to provide decidability proofs for a large class of
substructural logics.
-------------------------------------------------------------------------------
TR-ARP-12-94
Minlog
John Slaney
14 pages
The program minlog is a theorem prover for propositional minimal and
intuitionist logic, based on a cut-free sequent calculus. It achieves speed
more through careful coding than by incorporating sophisticated logical
techniques. It makes use of certain extra (derivable) rules to
shorten proofs in trivial ways, and it avoids some searching by not working on
the same sequent twice during the same proof search and by not trying to prove
sequents which are not classical tautologies. Proofs may be displayed in a
Fitch-style natural deduction format.
As well as being a tool for the logical investigation of constructive systems,
minlog is put forward as representing the baseline for high performance
theorem proving in this area.
The program, with sources, Makefile, documentation and `man' page, is
available by anonymous ftp from arp.anu.edu.au.
-------------------------------------------------------------------------------
TR-ARP-01-95
Intuitionistic Logic Redisplayed
Rajeev Gore'
34 pages
We continue the study of Belnap's Display Logic. Specifically, we
show that the boolean-tense-modal setting of Wansing and Kracht not
only allows us to ``redisplay'' intuitionistic logic but also allows
us to display superintuitionistic (intermediate) logics by using the
underlying Kripke semantics for these logics. The resulting Gentzen
systems inherit Belnap's cut-elimination and subformula properties,
but also inherit the caveat that these two properties no longer
*immediately* imply decidability. That is, although cut-elimination
now comes for free, we now have to work a lot harder to obtain
decidability. The systems pave *one* way for a proof-theoretical
study of subintuitionistic logics, superintuitionistic logics and
even hybrids like intuitionistic modal logics in one Display Logic
framework.
-------------------------------------------------------------------------------
TR-ARP-02-95
Realistic Belief Revision
Greg Restall and John Slaney
12 pages
In this paper we consider the implications for belief revision of weakening
the logic under which belief sets are taken to be closed.
A widely held view is that the usual belief revision functions are highly
classical, especially in being driven by consistency. We show that, on the
contrary, the standard representation theorems still hold for paraconsistent
belief revision. Then we give conditions under which consistency is preserved
by revisions, and we show that this modelling allows for the _gradual_
revision of inconsistency.
-------------------------------------------------------------------------------
TR-ARP-03-95
Negation in Relevant Logics (How I stopped worrying
and learned to love the Routley Star)
Greg Restall
25 pages
Negation raises three thorny problems for anyone seeking to
interpret relevant logics. The frame semantics for negation in relevant
logics involves a `point shift' operator *. Problem number one is the
interpretation of this operator. Relevant logics commonly interpreted
take the inference from A and ~AvB to B to be invalid,
because the corresponding relevant conditional A&(~AvB) -> B
is not a theorem. Yet we often make the inference from A and ~AvB
to B, and we seem to be reasoning validly when we do so.
Problem number two is explaining what is really going on here. Finally,
we can add an operation which Meyer has called _Boolean negation_ to
our logic, which is evaluated in the traditional way: x |= -A if and
only if not(x |= A). Problem number three involves deciding which is
the `real' negation. How can we decide between orthodox negation and the
new, `Boolean' negation. In this paper, I present a new interpretation
of the frame semantics for relevant logics which will allow us to give
principled answers to each of these questions.
-------------------------------------------------------------------------------
TR-ARP-04-95
Canonicity for Intensional Logics without Iterative Axioms
Timothy Surendonk
8 pages
David Lewis proved in 1974 that all logics without iterative axioms are
weakly complete. In this paper we extend Lewis's ideas and provide a proof
that such logics are strongly complete.i This paper also discusses the
differences between relational and neighborhood frame semantics and poses
a number of open questions about the latter.
-------------------------------------------------------------------------------
TR-ARP-05-95
Combining Possibilities and Negations
Greg Restall
16 pages
Combining non-classical (or `sub-classical') logics is not easy,
but it is very interesting. In this paper, we combine nonclassical
logics of negation and possibility (in the presence of conjunction and
disjunction), and then we combine the resulting systems with
intuitionistic logic. We will find that Kracht's results on
the undecidability of classical modal logics generalise to a
non-classical setting. We will also see conditions under which
intuitionistic logic can be combined with a non-intuitionistic negation
without corrupting the intuitionistic fragment of the logic.
-------------------------------------------------------------------------------
TR-ARP-06-95
A Uniform Display System for Intuitionistic and Dual
Intuitionistic Logic
Rajeev Gore'
15 pages
We give a way to ``display'' propositional intuitionistic and
dual-intuitionistic logic in one uniform setting. We show how the
usual ``singletons on the right'' restriction of Gentzen's LJ, and the
dual ``singletons on the left'' restriction can be mimicked in Display
Logic. The resulting Display System JDJ captures a hybrid logic that
permits reasoning with partial and paraconsistent knowledge since it
contains two negations - and ~ with the following properties: A \/ -A
is not a theorem; A /\ ~A is not a contradiction; A /\ - A is a
contradiction; and A \/ ~ A is a theorem. We then show how to obtain a
Display system for Classical Logic by the addition of structural rules
only.
Keywords: logical and mathematical models for AI, paraconsistent
logics, intuitionistic logic, hybrid logics, automated reasoning.
-------------------------------------------------------------------------------
TR-ARP-07-95
On the Completeness of Classical Tense Display Logic
8 pages
We give a purely syntactic proof of the completeness of classical
tense display logic DlKt: the sequent X |- Y is provable in
DlKt iff the formula T(X |- Y) is a theorem of minimal
tense logic Kt. Along the way we show how to relate Kracht's
structural rule for seriality to Wansing's one. Finally we observe a
trivial way to obtain the same system using different primitives.
-------------------------------------------------------------------------------
TR-ARP-08-95
SRS-II: Proceedings of the Second Symbolic Reasoning Systems Workshop
Editor: Rajeev Gore'
? pages
These are the papers presented at the Second Symbolic Reasoning
Systems Workshop held on April 21-22 1995, hosted by the Automated
Reasoning Project at the Australian National University in
Canberra.
-------------------------------------------------------------------------------
TR-ARP-09-95
Relevant Entailment and Modal Realism
Greg Restall
4 pages
In this short note I show how an account of relevant entailment can be
uncovered from the metaphysics of Modal Realism. This is surprising, as
it was previously thought that for modal realism, propositions must be
sets of possible worlds, and hence, necessarily equivalent propositions
must be identified.
-------------------------------------------------------------------------------
TR-ARP-10-95
A Non-Standard Injection Between Canonical Frames
Timothy J. Surendonk
10 pages
In this paper the ultrafilter properties of canonical frames are used to
produce a non-standard map between canonical frames of different
cardinalities. While this map is not a p-morphism, it is presented
as a step towards the full understanding of these structures.
-------------------------------------------------------------------------------
TR-ARP-11-95
MaGIC, Matrix Generator for Implication Connectives: Release 2.1 Notes and
Guide
John Slaney
88 pages
This is the documentation for release 2.1 of the program MaGIC (Matrix
Generator for Implication Connectives). It is also included with the source
of the program which is available from arp.anu.edu.au by ftp. MaGIC allows the
user to specify a system of logic as a Hilbert system with axioms and rules of
inference, and it then searches for small algebraic models of that logic.
Many axioms involving standard connectives are hard-coded, and a number of
logics defined in terms of them are made available. Further connectives and
further axioms and rules may be defined by the user. It is easy to customise
MaGIC by adding code to implement more axioms and more logics. The
documentation explains how to do this.
Release 2.1 is a considerable advance on release 2.0 which was made three
years ago. All current MaGIC users are urged to upgrade to 2.1 now, as 2.0
will not be actively supported in future.
-------------------------------------------------------------------------------
TR-ARP-12-95
Solving the display problem via residuation
Rajeev Gore
35 pages
The ``display problem'' of Belnap is an attempt to compare and
contrast the P-scheme of Belnap and the A-scheme of Wansing, each
of which have the display property. Restall has recenly shown that
relevant logics can be better displayed using a third scheme. We
show that the C-scheme presented here is a generalisation of all of
these schemes by showing how to obtain each of the other schemes,
plus other related cousins, all from the C-scheme. We then give a
systematic method for obtaining other schemes, all based on the
algebraic notions of Galois connections, residuation, and their
duals. We thus begin the task of explicitly connecting Belnap's
Display Logic and Dunn's Gaggle Theory.
-------------------------------------------------------------------------------
TR-ARP-13-95
Semantically Constrained Condensed Detachment is Incomplete
John Slaney and Timothy J. Surendonk
8 pages
In reporting on the theorem prover SCOTT (Slaney, SCOTT: A Semantically
Guided Theorem Prover, Proc. IJCAI, 1993) we suggested semantic constraint
as as an appropriate mechanism for guiding proof searches in propositional
systems where the rule of inference is condensed detachment---a generalisation
of Modus Ponens. Such constrained condensed detachment is closely analogous to
semantic resolution. This paper exhibits an example which shows that
semantically constrained condensed detachment is incomplete. That is, there
are formulae deducible by means of condensed detachment which are not
deducible when the semantic constraint is imposed. This answers an open
question from our 1993 paper.
-------------------------------------------------------------------------------
TR-ARP-14-95
Paraconsistent Logics!
Greg Restall
7 pages
In this note I respond to Hartley Slater's argument (JPL, August 1995) to
the effect that there is no such thing as paraconsistent logic. Slater's
argument trades on the notion of contradictoriness in the attempt to show
that the negation of paraconsistent logics is merely a subcontrary
forming operator and not one which forms contradictories. I will show
that Slater's argument fails, for two distinct reasons. Firstly, the
argument does not consider the position of non-dialethic paraconsistency
(which rejects the possible truth of any contradictions). Against this
position Slater's argument has no bite at all. Secondly, while the
argument does show that for dialethic paraconsistency (according to which
contradictions _can_ be true), certain other contradictions must be
true, I show that this need not deter the dialethic paraconsistentist from
their position.
-------------------------------------------------------------------------------
TR-ARP-15-95
Tableau Methods for Modal and Temporal Logics.
85 pages.
A handbook chapter on this subject.
-------------------------------------------------------------------------------
TR-ARP-16-95
Rajeev Gore and Wolfgang Heinle and Alain Heuerding.
Relations Between Propositional Normal Modal Logics: an overview.
26 pages.
The modal logic literature is notorious for multiple axiomatisations
of the same logic and for conflicting overloading of axiom names. Many
of the interesting interderivability results are still scattered over
the often hard to obtain classics. We catalogue the most interesting
axioms, their numerous variants, and explore the relationships between
them in terms of interderivability as both axiom (schema) and as
simple formulae. In doing so we introduce the Logics Workbench (LWB,
see http://lwbwww.unibe.ch:8080/LWBinfo.html!),
a versatile tool for proving theorems in numerous propositional
(nonclassical) logics. As a side effect we fulfill a call from the
modal theorem proving community for a database of known theorems.
-------------------------------------------------------------------------------
TR-ARP-17-95
John Slaney and Sylvie Thiebaux.
Blocks World Tamed: Ten thousand blocks in under a second.
27 pages.
Blocks World (BW) has been a standard example of a planning domain for almost
thirty years, and it is still commonly used to illustrate the capabilities
both of formalisms and of planners. As a minimum, therefore, we should know
certain basic things about the domain. It is clear that BW planning, in the
sense of finding some plan or other, is trivial, and it was shown in 1991 that
finding optimal (shortest) plans is NP hard. Various polynomial time
algorithms for approximating optimal BW planning exist, and there have been
attempts to implement these domain-specific methods in more general planning
frameworks. Here we report new complexity bounds for some of the approximation
algorithms, and discuss experimental results obtained with randomly generated
BW problems.
The work reported here greatly extends that described in TR-ARP-7-94.
-------------------------------------------------------------------------------
TR-ARP-18-95
John Slaney.
Generating Random States of Blocks World.
6 pages.
This is a companion piece to TR-ARP-17-95, and forms the documentation to one
of the programs used in experiments reported there.
The program BWSTATES generates a random sequence of states of the traditional
planning domain Blocks World (BW). These are useful for testing, evaluating
and illustrating both action formalisms and implementations of planning
systems. Contrary to what might be expected, it is not entirely trivial to
generate the states *randomly* in the sense that every state of the
specified size has the same probability of being generated. States generated
by BWSTATES have been used in experiments on near-optimal BW planning with up
to ten thousand blocks.
BWSTATES is available from ftp://arp.anu.edu.au/pub and comes with sources,
Makefile, README, online `man' page and this documentation.
-------------------------------------------------------------------------------
TR-ARP-19-95
Rajeev Gore.
Cut-free Display Calculi for Relation Algebras.
12 pages.
We give a propositional cut-free Gentzen-like calculus for relation
algebras using Belnap's Display Logic. The calculus extends trivially
to cater for a large class of axiomatic extensions of relation
algebras where the axioms appear as purely structural rules. The
calculus incorporates features of Relevant Display Logics and Modal
Display Logics, highlighting the relationship between relation
algebras and substructural logics.
-------------------------------------------------------------------------------
TR-ARP-20-95
Greg Restall.
Consequences of Negations.
10 pages.
This paper studies the behaviour of different consequence relations
on the one frame of points (situations, theories, worlds, or whatever).
I show how a frame of incomplete and inconsistent points might support
not only a finely-grained `relevant' consequence relation, but also
more classical coarsely-grained consequence relations. I sketch the
interactions between such relations, and I give a simple proof theory
which is sound and complete with respect to its intended semantics.
-------------------------------------------------------------------------------
TR-ARP-21-95
Greg Restall.
Lukasiewicz, Supervaluations and the Future.
6 pages.
In this paper I consider an interpretation of future contingents which
motivates a unification of a Lukiasiewicz-style logic, and the more classical,
supervaluational semantics. This in turn motivates a new non-classical logic
modelling what is ``made true by history up until now''. I give a simple
Hilbert-style proof theory, and a soundness and completeness argument for the
proof theory with respect to the intended models.
-------------------------------------------------------------------------------
TR-ARP-22-95
Greg Restall.
Display Logic and Gaggle Theory.
9 pages.
This paper is a revised version of a talk given at the _Logic and Logical
Philosophy_ conference in Poland in September 1995. In it, I sketch the
connections between Nuel Belnap's Display Logic and J. Michael Dunn's
Gaggle Theory.
-------------------------------------------------------------------------------
TR-ARP-01-96
Timothy Surendonk
Isomorphisms Between Canonical Frames.
10 pages
This paper looks at the question of what kinds of automorphisms
and isomorphisms can exist within and between canonical frames
for modal logics. Specifically, this paper is able to partially
answer the question posed by the author in TR-ARP-10-95 of whether
the canonical frame for L over a language of size omega_1
is isomorphic to the canonical frame for L over a language of size
omega in the presence of the extra-ZFC axiom ``2^omega=2^omega_1.''
We answer the question in the negative for all logics below S5 and
for all logics satisfying a natural condition. In addition we look at
automorphisms and show that while canonical frames for S5 in particular,
and logics of bounded alternative in general, have many non-standard
automorphisms, the logics satisfying the aforementioned natural condition
have none.
-------------------------------------------------------------------------------
TR-ARP-02-96
John K. Slaney, Robert K. Meyer and Greg Restall
Linear Arithmetic Desecsed
7 pages
In classical and intuitionistic arithmetics, any formula implies a true
equation, and a false equation implies anything. In weaker logics fewer
implications hold. In this paper we rehearse known results about the
relevant arithmetic R#, and we show that in linear arithmetic LL# by
contrast false equations never imply true ones. As a result, linear
arithmetic is _desecsed_. A formula A which entails 0=0 is a secondary
equation; one entailed by ~(0=0) is a secondary unequation. A system of
formal arithmetic is secsed if every extensional formula is either a
secondary equation or a secondary unequation. We are indebted to the
program MaGIC for the simple countermodel SZ7, on which 0=1 is not a
secondary formula. This is a small but significant success for
automated reasoning.
-------------------------------------------------------------------------------
TR-ARP-03-96
John Slaney
KD45 is not a Doxastic Logic
9 pages
The modal logic KD45 is frequently presented as the standard account of the
logic of belief for a single agent, where perhaps that agent is viewed as
having the doxastic properties of a deductive database. However, KD45 is
absurdly strong for such a reading. Specifically,
* K, D and 5 together are logically incoherent, even as an
account of the theory of a trivial database.
* K and 5 together make nonsense of the motivating concepts
of belief and introspection.
* K and D together contradict certain simple empirically
observable facts.
In the light of these observations, it is unacceptable that KD45 should
continue to be paraded as any kind of doxastic logic. This paper recommends
that the objections to KD45 be taken seriously and that the ``standard''
account be revised accordingly. It is suggested that such a revision will
force a major shift in the theory of epistemic and doxastic logic.
-------------------------------------------------------------------------------
TR-ARP-04-96
Timothy Surendonk
Neighbourhoods, Ultrafilters and Canonicity
7 pages
This paper will remind the reader of neighbourhood semantics for modal logics,
compare them with relational semantics, and then look at some questions about
neighbourhood semantics that have been answered, and some which are still
open. We will then introduce `ultrafilter semantics', a way of expressing all
sets over a canonical frame in an `effable' way. This provides us with a
conceptually easy way of dispatching some questions about intensional
logics. In particular, we show that all non-iterative intensional logics are
canonical and we go on to indicate how we can use ultrafilter semantics to
demonstrate the canonicity of the Sahlqvist Logics.
-------------------------------------------------------------------------------
TR-ARP-05-96
Timothy Surendonk
Expressing Sets with Ultrafilters and the Canonicity of the Sahlqvist Logics
9 pages
This paper will look at Sahlqvist's theorem in a new way. We introduce and
investigate a `skewed' type of semantics for modal logics over their canonical
frames. We will then use this semantics to describe every subset of a
canonical frame, we will show that the semantics respects all Sahlqvist
formulae, and we will then conclude that the Sahlqvist logics are
canonical. This will be accomplished without referring to any first order
properties of the canonical accessibility relation.
-------------------------------------------------------------------------------
TR-ARP-06-96
John Slaney and Sylvie Thiebaux
How Best to Put Things on Top of Other Things
12 pages
We give an algorithm which optimally solves planning problems in the Blocks
World, and report experimental investigations of its behaviour. One result is
the detection of a peak in the difficulty of the problems around a transition
from problems with a few tall towers to problems with many short ones. The
work reported here builds on that described in TR-ARP-17-95.
-------------------------------------------------------------------------------
TR-ARP-07-96
Graham Priest, Timothy J. Surendonk, and Koji Tanaka
An Error in Grove's Proof
4 pages
This note points out an error in Grove's proof that the Sphere
Semantics satisfy the AGM postulates (+7 and +8) for belief revision
and gives two ways of repairing the proof.
-------------------------------------------------------------------------------
TR-ARP-08-96
Greg Restall
Notes on Situation Theory and Channel Theory
18 pages
These are the notes for a workshop on Situation Theory and Channel
Theory, given at the 1996 Information Theoretic Approaches to Logic,
Language and Computation, in Regent's College, London. The notes
describe the basic features of situation theory and channel theory,
and indicate connections to modal logic, intuitionistic logic,
relevant logics and the Lambek calculus.
-------------------------------------------------------------------------------
TR-ARP-01-97
John Slaney and Robert Meyer
Logic for Two: The Semantics of Distributive Substructural Logics
This is an account of the semantics of a family of logics whose paradigm
member is the relevant logic R of Anderson and Belnap. The formal semantic
theory is well worn, having been discussed in the literature of such logics
for over a quarter of a century. What is new here is the explication of that
formal machinery in a way intended to make sense of it for those who have
claimed it to be esoteric, `merely formal' or downright impenetrable. Our
further goal is to put these logics in the service of practical reasoning
systems, since the basic concept of our treatment is that of an agent a
reasoning to conclusions using as assumptions the theory of agent b, where
a and b may or may not be the same. This concept is fundamental to
multi-agent reasoning.
-------------------------------------------------------------------------------
TR-ARP-02-97
Bernhard Beckert and Rajeev Gore'
Labelled Tableaux for Propositional Modal Logics
We present a sound, complete, modular and ``lean'' labelled
tableau calculus for many propositional modal logics, where the labels
contain ``free'' and ``universal'' variables. Our ``lean''
Prolog implementation is not only surprisingly short, but compares
favourably with other considerably more complex implementations for
modal deduction.
-------------------------------------------------------------------------------
TR-ARP-03-97
Nicolette Bonnette and Rajeev Gore'
Labelled Sequents for Propositional Tense Logics
We present an extension of the well-known method of labelled tableau
to handle tense logics. The sequent system is designed specifically
for a lean implementation.
-------------------------------------------------------------------------------
TR-ARP-04-97
Timothy J. Surendonk
Revising Some Basic Proofs in Belief Revision
This paper reobtains Grove's results (from his 1988 paper through) means which
are hopefully clearer and more illustrative of the underlying notions. Also,
the proofs are worked through in enough details that possible errors in Grove's
proof are clearly avoided. The paper concludes with a discussion on elementary
(or closed) systems of spheres and it notes that each revision function can
be given by such a system.
-------------------------------------------------------------------------------
TR-ARP-05-97
Timothy J. Surendonk
Canonicity for Intensional Logics with Even Axioms
This paper looks at the concept of neighborhood canonicity introduced by
Brian Chellas. We follow the lead of the author's paper where it was shown
that every non-iterative logic is neighborhood canonical and here we will
show that all logics whose axioms have a simple syntactic form---no
intensional operator is in boolean combination with a propositional
letter---and which have the finite model property are neighborhood canonical.
One consequence of this is that KMcK, the McKinsey logic, is nieghborhood
canonical, an interesting counterpoint to the results of Robert Goldblatt and
Xiaoping Wang who showed, respectively, that KMcK is not relational canonical
and that KMcK is not relationally strongly complete.
-------------------------------------------------------------------------------
TR-ARP-06-97
Pragati Jain
Undecidability of Relevant Logics
The question of the existence of a decision procedure for determining
whether formulas of a given logic are theorems of that logic is an
important one. Linial and Post showed in the late 1940's that undecidable
propositional logics do exist, but for many years all known examples of
such logics were ones that had been constructed explicitly for the purpose
of displaying undecidability. Indeed, Harrop in 1965 commented that "all
'philosophically interesting' propositional calculi for which the decision
problem has been solved have been found to be decidable..."
For over twenty years the decision problem for the principal relevant
logics remained open, and the problem was for many years regarded to be THE
outstanding open problem for relevant logics. It was finally solved by
Urquhart in 1984 in the negative: the relevant logic R and many of it's
neighbours are undecidable.
The ideas for the proof came from his earlier proof in of the
undecidability of the non-relevant logic KR, which was published in 1983,
and which we present in Chapter 3, as motivation for the methods of
Urquhart's general undecidability result. The proof relies on the ties
between a semantics for KR and projective spaces, and uses a result proved
by Lipshitz and independently by Hutchinson that the word problem for
modular lattices is unsolvable. Lipshitz's method uses the L-number
construction of Von Neumann; we exhibit the Lipshitz proof in Chapter 4,
and provide in an Appendix an informal geometric interpretation of Von
Neumann's L-number construction. Finally in Chapter 5 we give a modified
(and somewhat simplified and more comprehensive) version of Urquhart's 1984
result, which again draws heavily on the methods and results of Lipshitz.
-------------------------------------------------------------------------------
TR-ARP-07-97
Rajeev Gore'
Gaggles, Gentzen and Galois: Cut-free Display Calculi and Relational Semantics for Algebraizable Logics.
We show how the Gaggle Theory of Dunn gives a Gentzen-style proof
theory for many non-classical logics via the Display Logic of
Belnap. At the heart of both systems lie the algebraic notions of
residuation, Galois connections, and their duals.
-------------------------------------------------------------------------------
TR-ARP-08-97
Rajeev Gore'
Substructural Logics on Display
Substructural logics are traditionally obtained by dropping some or
all of the structural rules from Gentzen's LK or LJ. It is well
known that one can start with the Lambek Calculus and obtain,
exponential-free cyclic noncommutative linear, exponential-free
linear, relevant, BCK, and intuitionistic logics in an incremental
way. Each also has a classical counterpart. But there seems to be no
systematic attempt to do this in one single calculus by the addition
of purely structural rules to some constant core. We remedy this
situation by giving a single cut-free Display calculus for the
Bi-Lambek Calculus such that all these logics are obtained by the
incremental addition of purely structural rules. By using the
Gaggle Theory of Dunn we outline a (usually ternary) relational
semantics for each of these logics. Finally we follow a suggestion
of Lambek to show that exponentials can also be added to all our
logics as long as their only task is to embed intuitionistic
logic. To extend these substructural logics by real modalities is
more difficult.
-------------------------------------------------------------------------------
TR-ARP-09-97
John Slaney and Sylvie Thiebaux
Phase Transitions and Optimality: Sense and Nonsense
We study the hardness of finding an optimal plan in the Blocks World (BW). As
expected, there is an easy-hard-easy pattern in terms of the length of the
solution: problems with short solutions and problems requiring very long plans
are both easy to solve optimally. Our investigations relate this phenomenon to
a common underlying cause for both medium plan length and hard optimisation
problems. We offer some thoughts as to a qualitative explanation of
this. Along the way, we consider and dismiss another approach of associating
hardness with a phase transition in the probability of the existence of a
solution of given length. That approach we consider to be flawed, and we
believe that researchers on phase transition phenomena should beware of the
trap it opens.
-------------------------------------------------------------------------------
TR-ARP-10-97
Paul Wong
Weak Aggregative Modal Logics With Multi-ary Modal Operators
In this paper we generalize the Apostoli-Brown strategy developed
in [ab:95] to show the completeness of a descending chain of
weak aggregative modal logics with multi-ary modal operators.
The logics presented here are generalization of the weak aggregative
unary modal logics developed by Jennings and Schotch in the 80's.
-------------------------------------------------------------------------------
TR-ARP-01-98
Nicolette Bonnette and Rajeev Gore'
A Labelled Sequent System for Tense Logic Kt
The method of labelled tableaux for proof search in modal logics is
extended and modified to give a labelled sequent system for the tense
logic Kt. Soundness and completeness proofs are sketched, and results
of an initial lean Prolog implementation in the programming style of
leanTAP are presented. The sequent system is modular in that small
modifications capture anyh combination of the reflexive, transitive,
euclidean, symmetric and serial extensions of Kt.
-------------------------------------------------------------------------------
TR-ARP-02-98
Matthias Fuchs
Automatic Selection of Search-guiding Heuristics for Theorem Proving
Theorem proving essentially amounts to solving search problems.
The intricacy of these in general undecidable problems makes
the use of appropriate search-guiding heuristics indispensable.
However, the appropriateness of a heuristic critically depends
on the problem to be solved. Given a set of heuristics to choose
from, selecting a suitable heuristic is hence a crucial, but also
a very difficult task. It is usually taken care of by a proficient
user, because it is very hard to determine the suitability of a certain
heuristic based on a given problem to be solved. We propose here to
automate the selection of heuristics using machine-learning techniques
which ground their decisions on past problem-solving experience.
Experimental studies conducted in a very difficult area of theorem proving,
namely equational reasoning, demonstrate the capacity of the techniques and
underline their potential to be a very useful tool for eliminating human
interaction requiring expert knowledge.
-------------------------------------------------------------------------------
TR-ARP-03-98
Jacques Riche and Robert K Meyer
Kripke, Belnap, Urquhart and Relevant Decidability & Complexity
This paper is temporarily withdrawn. Here is its abstract.
The first philosophically motivated sentential logics to be proved
undecidable were relevant logics like R and E. But we deal here with
important decidable fragments thereof, like R->. Their decidability
rests on S. Kripke's gentzenizations, together with his central
combinatorial lemma. Kripke's lemma has a long history and was
reinvented several times. It turns out equivalent to and a
consequence of Dickson's lemma in number theory, with antecedents
in Hilbert's basis theorem. Dickson's lemma guarantees termination of
Buchberger's algorithm that computes the Groebner bases of polynomial
ideals. Our preferred form here of Dickson-Kripke is the Infinite
Division Principle (IDP). These principles have been used to show all
of LR decidable, forming the basis of the computer program KRIPKE.
-------------------------------------------------------------------------------
TR-ARP-04-98
Stephane Demri and Rajeev Gore
Display Calculi for Logics with Relative Accessibility Relations
We define cut-free display calculi for knowledge logics where an
indiscernibility relation is associated to each set of agents, and
where agents decide the membership of objects using this
indiscernibility relation. To do so, we first translate the logics
into polymodal logics axiomatised by primitive axioms and then use
Kracht's results on properly displayable logics to define the
display calculi.
Apart from these technical results, we argue that Display Logic is a
natural framework to define cut-free calculi for many other logics
with relative accessibility relations.
-------------------------------------------------------------------------------
TR-ARP-05-98
Hongxue Wang and John Slaney
On Generalities of Intelligent Systems
This paper reports some further results from our ontological
investigations into generalities of intelligent systems.
Different from that discussed in our earlier papers, in this
paper, we present our recent discovery of a generic theory of
intelligent systems, and point out two advantages of this
theory and derived techniques: to understand various existing
intelligent systems better, and to design various intelligent
systems more efficiently.
We would not dangerously claim that this theory could cover
every kind of intelligent systems, but we do hope this work
could resurrect research on generality of intelligence
and intelligent systems, and make some contributions to the
advancement of artificial intelligence as either a scientific
or a technical discipline.
-------------------------------------------------------------------------------
TR-ARP-06-98
John Slaney and Kahlil Hodgson
System Description: MSCOTT
MSCOTT (Multi-SCOTT) is a general purpose first order theorem
prover based on McCune's OTTER and having the same functionality
as OTTER. Like its predecessor SCOTT, it uses a model generator
to find small models of subsets of the clauses generated during
proof search. MSCOTT differs from SCOTT in that it generates and
uses several models simultaneously. This not only improves its
coverage of the useful semantic features of the problems it
addresses, but also changes its behaviour to the point where we
consider it a different prover. Naturally, its more intelligent
behaviour comes at a price: the extra time it must spend in
searching for models rather than in making deductions. The focus
of our current research on MSCOTT is the tradeoff between time
devoted to the two aspects of reasoning. Results already obtained
on the TPTP problems are encouraging.
-------------------------------------------------------------------------------
TR-ARP-07-98
Stephane Demri and Rajeev Gore
Cut-free Display Calculi for Nominal Tense Logics
We define cut-free display calculi for nominal tense logics
extending the minimal nominal tense logic (MNTL) by addition of
primitive axioms. To do so, we use the natural translation of MNTL
into the minimal tense logic of inequality L that is known to be
properly displayable by application of Kracht's results. The rules of
the display calculus dMNTL for MNTL mimic those of the display calculus
dL for L. Since dMNTL does not satisfy Belnap's condition (C8), we extend
Wansing's strong normalization theorem in order to get a similar theorem
for any extension of dMNTL by addition of structural rules satisfying Belnap's
conditions (C2)-(C7). The last part of the paper shows a weak Salhqvist-style
theorem for extensions of MNTL. By taking advantage of Kracht's techniques,
we then deduce that these extensions admit cut-free display calculi.
-------------------------------------------------------------------------------
TR-ARP-08-98
Matthias Fuchs
Finding Simpler Proofs in Logic Calculi
The design of search-guiding heuristics for theorem provers
centers on minimizing the time required to find any proof.
Mathematicians, however, are also interested in simple proofs.
Relevant simplicity criteria like proof length, for instance, hardly
play a role in the design of heuristics. In this report we present
heuristics designed to find simple proofs and empirically evaluate
their performance in the area of logic calculi. The experiments
demonstrate that significantly simpler proofs are found without
incurring increased search effort in many cases. As a matter of
fact, the search for simpler proofs very often succeeds faster
than a search guided by a "standard" heuristic based on counting
symbols.
-------------------------------------------------------------------------------
TR-ARP-09-98
Matthias Fuchs
A Data Mining Approach to Support the Creation of Loop Invariants
Using Genetic Programming
We describe a data-mining approach to creating central parts of
loop invariants. The approach is based on producing a trace table
by recording the values of program variables each time the condition
of a loop is evaluated. From this trace table, functional dependencies
between program variables can be extracted which may play a vital
role in loop invariants. The extraction process is accomplished through
the use of genetic programming which performs a symbolic regression
on the data contained by the trace table. We illustrate our approach
with examples.
-------------------------------------------------------------------------------
TR-ARP-10-98
Paul Wong
From Weak Satisfiability to n-Satisfiability On Hypergraphs
In this note we generalize A. Kolany's and R. Cowen's notions of
satisfiability on hypergraphs. The notion of n-satisfiability
on hypergraphs is developed here. We'll show that the compactness
property of n-satisfiability on hypergraphs is, in ZF set theory,
equivalent to the Prime Ideal theorem in Boolean algebra. Consequence
relations based on hypergraph will also be introduced and studied.
-------------------------------------------------------------------------------
TR-ARP-11-98
Paul Wong
Paraconsistent Inference and Preservation
The study of paraconsistent inference is the study of inference which
prohibits reasoning from inconsistent premises to arbitrary conclusions.
In this paper we examine a family of syntax based paraconsistent
inference relations and introduce a novel way to study and
compare these relations in terms of their preservational
properties.
-------------------------------------------------------------------------------
TR-ARP-01-99
Matthias Fuchs (ed.)
Automated Reasoning Day 1999
These are the extended abstracts of the talks given
at the Workshop on Automated Reasoning which was hosted by
the Automated Reasoning Project at the
Australian National University in Canberra on the 17 and 18 April 1999.
-------------------------------------------------------------------------------
TR-ARP-02-99
John Slaney
Why the Really Hard Problems are where they are
It is well known that many combinatorial search problems exhibit sharp
transitions between underconstrained phases where almost all instances
have many solutions and overconstrained phases where solutions are rare.
It is also well known that hard instances of such problems typically
cluster near the phase boundaries. This paper is concerned to correct
some popular misconceptions about these phenomena. Specifically, it is
observed that:
The existence of a phase transition where the number of solutions
per instance is close to 1 is merely a statistical effect due to the
randomness of the problem instances. It shows nothing remarkable
about search.
The association of a peak of hardness with the phase boundary is
trivially explicable. Therefore the existence of such a peak is in
itself of little significance.
The transitions do not normally occur at the 50% decision point.
Hardness does not generally peak at the phase boundary.
Despite the negative form of these observations, the purpose of this
paper is not to attack the research program in statistical properties
of search. Rather, it is to help distinguish between what is trivial
in that program and what is profound.
-------------------------------------------------------------------------------
TR-ARP-03-99
Sylvie Thiebaux and John Slaney
Predicting the Hardness of Optimisation Problems
We present a method for estimating the hardness of optimisation
problems (find a minimal cost solution to instance I) by observing
that of corresponding decision problems (has I a solution of cost
less than T). Decision is typically much easier than optimisation,
provided the threshold T is not too close to the optimal. Our
suggestion is to repeatedly solve easy decision cases, measure
their computational cost and extrapolate to the harder ones. An
investment of a few percent of the work required for optimisation
suffices to predict the latter within a small factor, even using a
very simple implementation of this idea.
-------------------------------------------------------------------------------
TR-ARP-04-99
Matthias Fuchs
Evolving Term Features: First Steps
Features play a central role in many areas of artificial intelligence
and in particular in machine learning. Mostly, features are provided by
the user. This is inevitable if the objects that are to be represented
with features are not accessible for the computer. Terms are a type of
data structure that is fundamental for a variety of problems such as,
for instance, automated theorem proving. In this report we propose to
automate the generation of term features using term patterns. The
search for a suitable set of features is conducted by a genetic
algorithm.
-------------------------------------------------------------------------------
TR-ARP-05-99
Stephane Demri and Rajeev Gore
Theoremhood Preserving Maps as a Characterisation of Cut
Elimination for Provability Logics
We define cut-free display calculi for provability (modal) logics that
are not properly displayable according to Kracht's analysis. We also
show that a weak form of the cut-elimination theorem (for these modal
display calculi) is equivalent to the theoremhood-preserving property
of certain maps from the provability logics into properly displayable
modal logics.
-------------------------------------------------------------------------
TR-ARP-01-00
Matthias Fuchs
An Evolutionary Approach to Support Web-Page Design
Arranging pictures or photographs on a wall or a sheet of paper can
be viewed as a layout problem that consists in placing a set of
rectangles on a large rectangle so that there are no overlaps, and
all edges are parallel to either the vertical or horizontal edge
of the large rectangle. Automating this process is sensible in
connection with web page design, in particular if frequent changes
occur. For web pages, it is possible and it makes sense to scale
pictures down so as to ensure that there is a solution to any
such layout problem. The goal then is to find a layout that
arranges the pictures in a way that is pleasing to the eye. We
propose to use genetic programming to evolve layouts, using a
representation similar to slicing tree structures, and a fitness
measure that incorporates the idea of aesthetic appeal as minimising
blank spaces.
-------------------------------------------------------------------------
TR-ARP-02-00
J. M. Davoren
Using modal logics for the formal analysis and synthesis
of hybrid control systems
The purpose of this paper is two-fold. We first give an overview of recent
work on the formal analysis and verification of hybrid systems, which are
dynamical systems with both discrete and continuous changes of state. We
then present new work on the use of poly-modal logics in the systematic
synthesis of hybrid control systems direct from formal specifications.
-------------------------------------------------------------------------
TR-ARP-03-00
Robert K. Meyer, Yoko Motohama, and Mariangiola Dezani-Ciancaglini
The Semanics of Entailment Omega
Abstract forthcoming
-------------------------------------------------------------------------
TR-ARP-04-00
John Slaney, Sylvie Thiebaux and Phil Kilby
Estimating the Hardness of Optimisation
Estimating computational cost is a fundamental issue in time-bounded
computation. We present a method for estimating the hardness of optimisation
problems (find a minimal cost solution to instance I) by observing that of
the corresponding decision problems (has I a solution of cost less than
threshold T). Provided T is not too close to the optimal, decision is
typically much easier than optimisation, yet knowing the hardness of the
former is useful for predicting the latter. The present paper reports an
experimental investigation of this idea, with encouraging results. An
investment of a few percent of the work required for optimisation suffices
for estimation within a small factor, even using a very simple implementation
of the method.
-------------------------------------------------------------------------
TR-ARP-05-00
S. van Bakel, M. Dezani-Ciancaglini, U. de'Liguoro, Y. Motohama
The Minimal Relevant Logic and the Call-by-Value Lambda Calculus
The minimal relevant logic B+, seen as a type discipline, includes an
extension of Curry types known as the intersection type discipline. We
will show that the full logic B+ gives a type assignment system which
produces a model of Plotkin's call-by-value lambda-calculus.
-------------------------------------------------------------------------
TR-ARP-06-00
John Slaney
Inside the Constrainedness of Search
Recent work on search has identified an intriguing feature dubbed the
constrainedness knife-edge by Walsh (Proc. AAAI-98, 406-411) whereby
overconstrained problems seem to become on average even more
constrained as the search goes deeper, while underconstrained ones
become less constrained. The present paper shows that while the
knife-edge phenomenon itself is real, many of the claims that have
been made about it are incorrect. It is not always associated with
criticality, it is not a function of the problem so much as of the
algorithm used to solve it, and it does not help to explain the
peculiar hardness of problem instances near phase transitions. Despite
the negative findings, the upshot is that Walsh's work has opened a
fascinating line of research which will surely repay further
investigation.
-------------------------------------------------------------------------
TR-ARP-07-00
Robert K. Meyer and Greg Restall
"Strenge" Arithmetics
In ENTAILMENT, Anderson and Belnap motivated their modification E of
Ackermann's strenge Implikation PI' as a logic of relevance and
necessity. The kindred system R was seen as relevant but not as
modal. Our systems of Peano arithmetic R# and omega arithmetic R##
were based on R to avoid fallacies of relevance. But problems arose as
to which arithmetic sentences were (relevantly) true. Here we base
analogous systems on E to solve those problems. Central to motivating
E is the rejection of fallacies of modality. Our slogan here for this
is, "No diamonds entail any boxes." Form the strenge Peano arithmetic
E# like R#, adding appropriate forms of the Peano axioms to
Ackermann's EQ. Extend E# to the strenge omega arithmetic E## by
adding the omega-rule A(0), A(1),... ==> (x)Ax. E# and E## make
explicit a rejection of "fallacies of modality" implicit in R#, where
already "equations" work like boxes and "unequations" like
diamonds. (And no "unequations" relevantly imply any "equations".) The
R# theory of secondary formulas extends straightforwardly to our
strenge arithmetics. Finally METAVALUING E## yields the strenge true
arithmetic TE#. TE# treats truth-functions and quantifiers
truth-functionally, settling sentences like 0=2 --> 0=1 by AFFIRMING
THEIR NEGATIONS (as Belnap once suggested).
------------------------------------------------------------------------
TR-ARP-08-00
Robert K. Meyer
What Entailment Can Do for Type Theory
Logics of entailment were developed for philosophical reasons before
recent work in type theory. Yet there is a confluence between
them. This confluence is evident at the logic B+, which was proposed
in 1972 as the minimal relevant logic. Yet a few years later an
essentially equivalent system was independently invented as a theory
of (non-Curry) intersection (and union) types. This paper suggests
several ways in which research in relevant logics can be adapted to
produce results (and perhaps even insights) for
type-theorists. Brady's depth relevance is one such. Another is
conservative Boolean extension from B+ to CB. Conversely the profound
technical understanding that has produced filter models for functional
theories definitively illumines the semantics of relevant logics.
-----------------------------------------------------------------------
TR-ARP-09-00
Matthias Fuchs and Geoff Sutcliffe
Homogeneous Sets of ATP Problems
This report describes how the homogeneity of sets of ATP problems
can be measured with respect to the performance of ATP systems.
Measuring homogeneity is important as a basis for empirical evaluation
of ATP systems and problems.
The method developed assigns problems to nodes in a graph, and finding
homogeneous sets of problems is reduced to finding maximal cliques in the
graph. The method is robust to the realities of empirical data collection.
A machine learning approach has been used to differentiate between types
of problems in situations where heterogeneity is apparent.
-----------------------------------------------------------------------
TR-ARP-10-00
J.M. Davoren and R.P. Gore
Bimodal Logics for Reasoning About Continuous Dynamics
We study a propositional bimodal logic consisting of two S4
modalities [ ] and [a], together with the
interaction axiom scheme [ ]p --> [ ]p. In the intended
semantics, the plain [ ] is given the McKinsey-Tarski
interpretation as the interior operator of a topology, while the
labelled [a] is given the standard Kripke semantics
using a reflexive and transitive binary relation R_a. The
interaction axiom expresses the property that the relation R_a
is \emph{lower semi-continuous} with respect to the topology. The
class of topological Kripke frames axiomatised by the logic includes
all frames over Euclidean space where R_a is the positive flow
relation of a differential equation. We establish the completeness
of the axiomatisation with respect to the intended class of
topological Kripke frames, and investigate tableau calculi for the
logic, although decidability is still an open question.
-----------------------------------------------------------------------
TR-ARP-11-00
G. Sutcliffe and M. Fuchs and C. Suttner
Progress in Automated Theorem Proving, 1997-1999
Despite some impressive individual achievements, the extreme difficulty
of Automated Theorem Proving (ATP) means that progress in ATP is slow
relative to, e.g., some aspects of commercial information technology.
The (relatively) slow progress has two distinct disadvantages.
First, for the researchers, it is difficult to determine if a
direction of investigation is making a meaningful contribution.
Second, for unaware observers, a lack of progress leads to a loss of
interest and confidence in the field.
A serious outcome of this loss of interest and confidence has been
the withdrawal of significant funding for ATP research.
In this context of slow progress, it is important that progress in
ATP be measured, monitored, and recognized.
This paper presents quantitative measures that show progress in ATP,
from mid-1997 to the end of 1999.
The measures are based on collected performance data from ATP systems.
-----------------------------------------------------------------------
TR-ARP-01-01
Jeremy E Dawson and Rajeev Gore
Mechanising Strong Normalisation for Display Calculi
We describe a mechanised proof of strong normalisation for the display
calculus for relation algebras in Isabelle/HOL. The proof requires
well-founded induction over three partial orders and generalises
easily to other display calculi.
-----------------------------------------------------------------------
TR-ARP-01-02
Robert K. Meyer and Dolph Ulrich
Perfect Words are Pleasing (and PLEASING is Perfect)
A word is SOUND, COMPLETE or PERFECT depending on how it is touch-typed.
We concentrate on perfect words, which are both sound and complete. A
word is perfect just in case each typing finger is used exactly once.
Example: PLEASING. We list a number of perfect words, most of them found
by computer search at Purdue University.
-------------------------------------------------------------------------
TR-ARP-01-03
Sylvie Thiebaux, Joerg Hoffmann, and Bernhard Nebel
In Defense of PDDL Axioms
There is controversy as to whether explicit support for PDDL-like
axioms and derived predicates is needed for planners to handle
real-world domains effectively. Many researchers have deplored the
lack of precise semantics for such axioms, while others have argued
that they are a non-essential feature which is best compiled away. We
propose an adequate semantics for PDDL axioms and show that they are
an essential feature by proving that it is impossible to compile them
away if we restrict the growth of plans and domain descriptions to be
polynomial. These results suggest that adding a reasonable
implementation to handle axioms inside the planner is beneficial for
the performance. Our experiments confirm this suggestion.
-------------------------------------------------------------------------
TR-ARP-02-03
Agnes Boskovitz, Rajeev Gore' and Markus Hegland
A Logical Formalisation of the Fellegi-Holt Method of Data Cleaning
The Fellegi-Holt method automatically ``corrects'' data that fail
some predefined requirements. Computer implementations of the method
were used in many national statistics bureaux but are less used now
because they are slow. We recast the method in propositional logic,
and show that many of its results are well-known results in
propositional logic. In particular we show that the Fellegi-Holt
method of ``edit generation'' is essentially the same as a technique
for automating logical deduction called resolution. Since modern
implementations of resolution are capable of handling large problems
efficiently, they might lead to more efficient implementations of
the Fellegi-Holt method.
-------------------------------------------------------------------------