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. -------------------------------------------------------------------------