Baumgartner P. Theory Reasoning in Connection Calculi
Подождите немного. Документ загружается.
Lecture Notes in Artificial Intelligence 1527
Edited by J.G. Carbonell and J. Siekmann
Subseries of Lecture Notes in Computer Science
Berlin
Heidelberg
New York
Barcelona
Hong Kong
London
Milan
Paris
Singapore
Tokyo
Peter Baumgartner
Theory Reasoning
in Connection Calculi
Series Editors
Jaime G. Carbonell, Carnegie Mellon University, Pittsburgh, PA, USA
J
¨
org Siekmann, University of Saarland, Saarbr
¨
ucken, Germany
Author
Peter Baumgartner
Universit
¨
at Koblenz-Landau, Institut f
¨
ur Informatik
Rheinau 1, D-56075 Koblenz, germany
E-mail: peter@uni-koblenz.de
Cataloging-in-Publication Data applied for
Die Deutsche Bibliothek - CIP-Einheitsaufnahme
Baumgartner, Peter:
Theory reasoning in connection calculi / Peter Baumgartner. - Berlin ;
Heidelberg ; New York ; Barcelona ; Hong Kong ; London ; Milan ; Paris ;
Singapore ; Tokyo : Springer, 1998
(Lecture notes in computer science ; 1527 : Lecture notes in artificial
intelligence)
ISBN 3-540-65509-3
CR Subject Classification (1998): I.2.3, F.4.1
ISBN 3-540-65509-3 Springer Berlin Heidelberg New York
This work is subject to copyright. All rights are reserved, whether the whole or part of the material is
concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting,
reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication
or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965,
in its current version, and permission for use must always be obtained from Springer-Verlag. Violations are
liable for prosecution under the German Copyright Law.
c
Springer-Verlag Berlin Heidelberg 1998
Printed in Germany
Typesetting: Camera-ready by author
SPIN 10692875 06/3142–543210 Printedonacid-free paper
Preface
Certainly, the ability to draw inferences is a central operation in any Artificial
Intelligence (AI) system. Consequently, automated deduction is one of the
most traditional disciplines in AI. One core technique, the resolution principle
[Robinson, 1965b] nowadays even seems to be standard knowledge for any
computer scientist.
Although resolution is particularly well suited for implementation on a
computer, it became clear soon after its invention that even more elaborate
techniques are needed to cope with the tremendous search space. One of these
techniques is theory reasoning, where the idea is to incorporate specialized
and efficient modules for handling general domain knowledge into automated
reasoning. These theory reasoning modules might, for instance, simplify a
goal, compute solutions, look up facts in a database, etc. Also, the most
suitable knowledge representation formalism might be used for this.
This book is on extensions of calculi for automated theorem proving to-
ward theory reasoning. It focuses on connection methods and in particular
on model elimination. An emphasis lies on the combination of such calculi
with theory reasoners to be obtained by a new compilation approach.
Several theory-reasoning versions of connection calculi are defined and
related to each other. In doing so, theory model elimination (TME) will be
selected as a base to be developed further. The final versions are search-space
restricted versions of total TME, partial TME, and partial restart TME.
These versions all are answer-complete, thus making TME interesting for
logic programming and problem-solving applications.
A theory reasoning system is only operable in combination with an (ef-
ficient) background reasoner for the theories of interest. Instead of hand-
crafting respective background reasoners, a more general approach – lineariz-
ing completion – is proposed. Linearizing completion enables the automatic
construction of background calculi suitable for TME-based theory reason-
ing systems from a wide range of axiomatically given theories, namely Horn
theories.
Technically, linearizing completion is a device for combining the unit-
resulting strategy of resolution with a goal-oriented, linear strategy as in
Prolog in a refutationally complete way.
VI Preface
Finally, an implementation extending the PTTP technique (Prolog based
Technology Theorem Proving) toward theory reasoning is described, and
the usefulness of the methods developed in this text will be experimentally
demonstrated.
This book was written during my employment
1
as a research assistant
at the institute for computer science at the University of Koblenz-Landau in
Germany. It is the revised version of a doctoral dissertation submitted and
accepted at this institute.
I would like to thank all those who contributed in this work in one way
or the other:
In the first place I am grateful to Ulrich Furbach. He conducted me to
scientific work, and he always found time for helpful discussions. His advice
and criticism pushed me ahead quite a few times.
Further, I wish to thank the other reviewers of my thesis: Peter Schmitt
(University of Karlsruhe, Germany), David Plaisted (University of North Car-
olina, USA), and Karin Harbusch (University of Koblenz-Landau, Germany),
who substituted Prof. Plaisted in the oral examination of my thesis.
It was really a great pleasure for me to spend the last few years in the com-
pany of my colleagues. J¨urgen Dix, Frieder Stolzenburg, and Stefan Br¨uning
(Technische Hochschule Darmstadt, Germany) read this lengthy text, and
several improvements resulted from their suggestions.
Several bright students supported me a lot through implementational
work and discussions. Katrin Erk, Michael K¨uhn, Olaf Menkens, Dorothea
Sch¨afer and Bernd Thomas never tired of turning my ideas into running code.
Koblenz, August 1998 Peter Baumgartner
1
Funded by the DFG (Deutsche Forschungsgemeinschaft) within the research pro-
gramme “Deduction”.
Contents
1. Introduction .............................................. 1
1.1 TheoryReasoning:Motivation ........................... 1
1.2 HistoricalNotes ........................................ 5
1.3 Further Reading........................................ 8
1.4 Overviewand ContributionsofthisBook.................. 9
2. Logical Background ....................................... 15
2.1 Preliminaries........................................... 15
2.2 Syntax ofFirst-Order Logic.............................. 17
2.3 SemanticsofFirst-OrderLogic........................... 20
2.4 ClauseLogic........................................... 27
2.4.1 TransformationintoClauseLogic................... 27
2.4.2 HerbrandInterpretations.......................... 30
2.4.3 Unification ...................................... 34
2.5 Theories............................................... 36
2.5.1 Sample Theories ................................. 38
2.5.2 PropertiesofTheories ............................ 41
2.5.3 Universal Theories and Herbrand Theory Interpretations 44
3. Tableau Model Elimination ............................... 49
3.1 ClausalTableaux....................................... 49
3.2 Inference Rules and Derivations .......................... 52
3.2.1 Answers......................................... 57
3.2.2 ClausalTableauxvs.BranchSets................... 58
3.3 Improvements.......................................... 60
3.3.1 Independence of the Computation Rule . . . . . . . . . . . . . 60
3.3.2 Regularity....................................... 61
3.3.3 Factorization .................................... 62
3.3.4 Reduction Steps.................................. 63
4. Theory Reasoning in Connection Calculi .................. 65
4.1 BasicsofTheoryReasoning.............................. 65
4.1.1 Total and Partial Theory Reasoning . . . . . . . . . . . . . . . . 68
4.1.2 InstancesofTheoryReasoning ..................... 72
VIII Contents
4.2 ATotalTheoryConnectionCalculus...................... 80
4.2.1 Theory Refuting Substitutions . . . . . . . . . . . . . . . . . . . . . 81
4.2.2 Definition of a Total Theory Connection Calculus . . . . 85
4.2.3 Soundness of TTCC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
4.3 Theory Model Elimination — Semantical Version . . . . . . . . . . . 90
4.3.1 Motivation ...................................... 90
4.3.2 Definition of Theory Model Elimination . . . . . . . . . . . . . 92
4.3.3 Relation to TTCC-Link . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
4.4 Total Theory Model Elimination — MSR-Version. . . . . . . . . . . 101
4.4.1 Complete and Most General Sets of T -Refuters . . . . . . 102
4.4.2 Definition ofTTME-MSR ......................... 106
4.4.3 Soundness and Answer Completeness of TTME-MSR . 109
4.4.4 Related Work.................................... 112
4.4.5 A Sample Application: Terminological Reasoning . . . . . 113
4.5 Partial Theory Model Elimination - Inference Systems Version 115
4.5.1 Theory InferenceSystems ......................... 118
4.5.2 Definition of PTME-I ............................ 120
4.5.3 Soundness and Answer Completeness . . . . . . . . . . . . . . . 123
4.5.4 An Application: Generalized Model Elimination . . . . . . 128
4.6 RestartTheoryModel Elimination........................ 129
4.6.1 Definition of Restart Theory Model Elimination . . . . . . 130
4.6.2 Soundness and Answer Completeness . . . . . . . . . . . . . . . 135
4.6.3 Regularity and First-Order Completeness . . . . . . . . . . . . 137
Other Refinements................................ 139
5. Linearizing Completion ................................... 141
5.1 Introduction ........................................... 142
5.1.1 Linearizing Completion and Theory Reasoning . . . . . . . 142
5.1.2 Related Work.................................... 143
5.1.3 Relation to Knuth-Bendix Completion . . . . . . . . . . . . . . 147
5.1.4 InformalDescriptionofthe Method................. 148
5.1.5 Linearizing Completion and Resolution Variants . . . . . . 153
5.1.6 Preliminaries .................................... 157
5.2 Inference Systems ...................................... 157
5.2.1 InitialInference Systems .......................... 160
5.2.2 Completeness of Initial Inference Systems . . . . . . . . . . . 162
5.2.3 Subderivations ................................... 163
5.3 Orderings and Redundancy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
5.3.1 Orderings on Nested Multisets with Weight . . . . . . . . . . 165
5.3.2 DerivationOrderings.............................. 167
5.3.3 Redundancy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168
5.4 TransformationSystems................................. 171
5.4.1 Limit Inference Systems........................... 174
5.4.2 FairnessandCompletion .......................... 175
5.5 Complexity-ReducingTransformationSystems ............. 177
Contents IX
5.6 Completeness .......................................... 180
5.6.1 Ground Completeness............................. 181
5.6.2 The Link to Theory Model Elimination . . . . . . . . . . . . . 183
5.6.3 First-OrderCompleteness ......................... 185
5.7 SampleTheories........................................ 186
5.7.1 Equality andParamodulation...................... 186
5.7.2 Equality plus Strict Orderings ..................... 189
5.7.3 ModalLogics .................................... 190
6. Implementation ........................................... 193
6.0.4 SCAN-IT........................................ 193
6.0.5 LC ............................................. 194
6.1 PROTEIN............................................. 195
6.1.1 High Inference Rate Based Theorem Proving . . . . . . . . . 195
6.1.2 The PTTP ImplementationTechnique .............. 196
6.2 PracticalExperiments................................... 200
7. Conclusions ............................................... 207
A. Appendix: Proofs ......................................... 211
A.1 Proofs for Chapter 4 — Theory Reasoning . . . . . . . . . . . . . . . . . 211
A.1.1 Completeness of TTME-MSR...................... 215
A.1.2 GroundCompletenessofPTME-I .................. 235
A.2 ProofsforChapter5 —LinearizingCompletion ............ 239
A.2.1 Section5.2—Inference Systems ................... 239
A.2.2 Section 5.3 — Orderings and Redundancy . . . . . . . . . . . 241
A.2.3 Section5.4—TransformationSystems.............. 246
A.2.4 Section 5.5 — Complexity-Reducing Transformation
Systems......................................... 250
A.2.5 Section5.6—Completeness ....................... 257
B. What is Where? .......................................... 263
List of Figures ................................................ 267
Bibliography .................................................. 269
Index ......................................................... 281
1. Introduction
1.1 Theory Reasoning: Motivation
Certainly, the ability to draw inferences is a central operation in any Artificial
Intelligence (AI) system. Consequently, automated deduction is one of the
most traditional disciplines in AI. A major goal of research here is to develop
general algorithms or semi-decision procedures for the solution of problems
formulated in first-order predicate logic. One core technique, the resolution
principle
[
Robinson, 1965b
]
nowadays seems to be even standard knowledge
of any computer scientist. Resolution made popular the use of clause logic and
of unification in theorem proving calculi. In particular, the use of unification
is a major point, as calculi were predominated at that time by reducing first
order logic to propositional logic by more or less blindly guessing ground
instantiations of formulae.
But soon after the invention of the resolution principle it became clear
that even more elaborate techniques are needed to cope with the tremendous
search space. One of these techniques is theory reasoning, where the idea is
to incorporate specialised and efficient modules for handling general domain
knowledge into automated reasoning. These theory reasoning modules might,
for instance, simplify a goal, compute solutions, lookup facts in a database,
etc. Also, the most suitable knowledge representation formalism might be
used for this.
Let us take a more technical point of view: suppose as given a set F of
predicate logic formulas and a predicate logic formula G. We would like to
know if G follows from the F , i.e. whether F |= G holds. In principle, any
complete predicate logic calculus can be used to semi-decide this question.
In a refined situation, G is of the form ∃xG
0
(for some formula G
0
), and the
task is to compute solutions for the variables x of the problem G. The calculi
developed in this book are answer complete, and hence allow to compute, in
a sense, all of them.
The emphasis in this book, however, is on theory reasoning: In a theorem
prover supporting theory reasoning, one can think of F as partitioned in
F = T∪F
G
(read T as “theory”), and T would be handled by a specialised
“background reasoner `
T
”, while F
G
and G would be treated by a general
first-order “foreground reasoner ` ”. Typically, these parts heavily interact
in the combined system `
`
T
(cf. Figure 1.1).
P. Baumgartner: Theory Reasoning in Connection Calculi, LNAI 1527 , pp. 1-13, 1998
Springer-Verlag Berlin Heidelberg 1998