Baumgartner P. Theory Reasoning in Connection Calculi
Подождите немного. Документ загружается.
B. What is Where? 265
Table of Foreground Calculi
The following foreground calculi are treated in this text:
Abbreviation Name, Inference Rules Definition
ME Model elimination
ME-Ext, Red
Def. 3.2.3, page 53
CC Connection calculus
CC-Ext, Red
Def. 3.2.3, page 53
TTCC Total theory connection calculus
TTCC-Ext
Def. 4.2.3, page 85
TTCC-Link Total theory connection calculus
with link condition
TTCC-Link-Ext
Def. 4.2.4, page 87
TME-Sem Theory Model elimination —
semantical version
TME-Sem-Ext (TTME-Sem-Ext,
PTME-Sem-Ext)
Def. 4.3.2, page 93
TTME-MSR Total Theory Model elimination —
MSR version
TTME-MSR-Ext
Def. 4.4.3, page 106
PTME-I Partial theory model elimination,
inference system version
PTME-I-Ext
Def. 4.5.4, page 120
PRTME-I Partial restart theory model
elimination, inference system
version
PDTME-I-Ext, Restart
Def. 4.6.3, page 131
266 B. What is Where?
Inferences and Derivation Relations
Notation Description Definition
P`
[p],σ,E
P
0
Inference in Foreground Calculus:
derive branch set P
0
from P, with
selected branch [p], substitution σ and
extending clauses E.
Def. 3.2.4, page 55
Extended Notations:
([p], Q) `
[p],K,σ,E
(Q
0
, Q)σ
TTCC-Link-Ext inference with key set K
and minimal T -refuter σ
Def. 4.2.4, page 87
([p], Q) `
[p],K,hR,σi,E
(Q
0
, Q)σ
TME-Sem-Ext inference with key set K
and minimal T -residue hR,σi
Def. 4.3.2, page 93
([p], Q) `
[p],K,σ,E
(Q
0
, Q)σ
TTME-MSR-Ext inference with key set
K and minimal most general T -refuter
σ ∈ MSR
T
(K)
Def. 4.4.3, page 106
([p], Q) `
[p],K,P →C,hR,σi,E
(Q
0
, Q)σ
PTME-I-Ext inference with key set K,
new variant P → C of an inference rule
from I and T -residue hR,σi
Def 4.5.4, page 120
([p
1
], Q
1
) `···`Q
n
Derivation in foreground calculus,
possibly subscribed by selected branch
etc.
Def. 3.2.4, page 55
K⇒
P →C, σ
Rσ
Minimal first-order theory inference
with rule P → C
Def. 4.5.2, page 118
L
1
⇒
∗
I,M,σ
L
n+1
Background derivation of L
n+1
from M
with top literal L
1
and substitution σ
Def. 4.5.5, page 123
P
0
⇒
P →
w
C, δ
C
0
Matching theory inference with rule
P →
w
C with weight w
Def. 5.2.2, page 158
I
0
`
S
I
1
`
S
···`
S
I
n
`
S
···
Deduction in transformation system S Def. 5.4.1,page 171
List of Figures
1.1 Principle of Theory Reasoning ............................... 2
1.2 A toy knowledge base. ...................................... 3
2.1 Relationships among theories. ................................ 44
3.1 A closed model elimination tableau. ........................... 51
3.2 A ME refutation corresponding to the tableau in Figure 3.1. .... 56
3.3 Mapping of chains to literal trees. ............................ 59
4.1 “Weaker-than” relation between the calculi of Chapter 4 ....... 66
4.2 A total theory extension step in the theory connection calculus. . . 69
4.3 A partial theory extension step in the theory connection calculus. 71
4.4 A Classification of Theory Reasoning. ......................... 72
4.5 Total theory extension step in the theory connection calculus. .... 85
4.6 Two inference steps of TTCC-Link. ........................... 94
4.7 A partial theory model elimination extension step. .............. 94
4.8 A snapshot from the refutation constructed in the proof of Theo-
rem 4.3.1. ................................................. 98
4.9 A PTME-I derivation. Missing key set literals are annotated at
the edges. ................................................. 124
4.10 A PRTME-I derivation. ..................................... 134
5.1 A problem-solving application of linearizing completion. ......... 144
5.2 Summary of Relationships between Knuth-Bendix completion and
linearizing completion. ...................................... 148
5.3 A non-linear unit-resulting refutation of {A, C}∪S. ............ 150
5.4 A linear unit-resulting refutation, using the new rule B,C → F. . . 151
5.5 The theory ES of equality and strict orderings with unary function
symbol f. ................................................. 161
5.6 The inference system I
0
(ES). ................................ 161
5.7 The transformation rules of the transformation system Lin. ..... 172
5.8 The theory of equality in a language with a 2-ary predicate symbol
P ......................................................... 186
5.9 A completed inference system for equality without function symbols.187
5.10 A completed inference system for the theory ES ................ 189
268 List of Figures
6.1 Runtime results for various provers on selected TPTP problems. . . 203
6.2 Runtime results for various provers on TPTP problems on group
theory and boolean algebra. ................................. 204
6.3 Runtime results for various provers for S4 theorems. ............ 205
A.1 Illustration of proof of Proposition 5.3.3. ...................... 244
A.2 Illustration of proof of Proposition 5.5.1 (ground case). ......... 251
A.3 A case in the proof of Proposition 5.5.3 (ground case). .......... 253
A.4 A case in the proof of Lemma 5.5.3 (ground case) .............. 256
A.5 Illustration of proof of Lemma 5.6.1 (ground case). ............. 259
Bibliography
[
Ait-Kaci and Nasr, 1986
]
H. Ait-Kaci and R. Nasr. LOGIN: A Logic Programming
Language with Built-in Inheritance. Journal of Logic Programming, 3:293–345,
1986.
[
Anderson and Bledsoe, 1970
]
R. Anderson and W. Bledsoe. A linear format for
resolution with merging and a new technique for establishing completeness. J.
of the ACM, 17:525–534, 1970.
[
Andrews, 1976
]
Peter B. Andrews. Refutations by Matings. IEEE Transactions
on Computers, C-25:193–214, 1976.
[
Antoniou and Langetepe, 1994
]
G. Antoniou and E. Langetepe. Applying SLD-
Resolution to a Class of Non-Horn Logic Programs. Bulletin of the IGPL,
2(2):231–243, 1994.
[
Apt and van Emden, 1982
]
K.R. Apt and M.H. van Emden. Contributions to the
Theory of Logic Programming. Journal of the Association for Computing Ma-
chinery, 29(3):841–862, 1982.
[
Astrachan and Stickel, 1992
]
Owen L. Astrachan and Mark E. Stickel. Caching
and Lemmaizing in Model Elimination Theorem Provers. In Kapur
[
1992
]
,
pages 224–238.
[
Bachmair and Ganzinger, 1990
]
L. Bachmair and H. Ganzinger. On Restrictions
of Ordered Paramodulation with Simplification. In Stickel
[
1990b
]
, pages 427–
441.
[
Bachmair and Ganzinger, 1994
]
L. Bachmair and H. Ganzinger. Rewrite tech-
niques for transitive relations. In Proc. 9th IEEE Symposium on Logic in Com-
puter Science, pages 384–393. IEEE Computer Society Press, 1994.
[
Bachmair and Ganzinger, 1998a
]
Leo Bachmair and Harald Ganzinger. Elimina-
tion of equality via transformation with ordering constraints. In Claude Kirch-
ner and H´el`ene Kirchner, editors, Automated Deduction — CADE 15, LNAI
1421, Lindau, Germany, July 1998. Springer-Verlag.
[
Bachmair and Ganzinger, 1998b
]
Leo Bachmair and Harald Ganzinger. Ordered
chaining calculi for first-order theories of transitive relations. Journal of the
Association for Computing Machinery, 1998. Revised Version of MPI-I-95-2-
009. To appear.
[
Bachmair et al., 1986
]
Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Or-
derings for equational proofs. IEEE, pages 346–357, 1986.
[
Bachmair et al., 1989
]
L. Bachmair, N. Dershowitz, and D. Plaisted. Completion
without failure. In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in
Algebraic Structures 2: Rewrite Techniques, pages 1–30. Academic Press, 1989.
[
Bachmair et al., 1992
]
L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Ba-
sic Paramodulation and Superposition. In Kapur
[
1992
]
, pages 462–476.
[
Bachmair, 1987
]
Leo Bachmair. Proof Methods for Equational Theories. PhD
thesis, University of Illinois at Urbana, U.S.A., 1987.
270 Bibliography
[
Bachmair, 1991
]
L. Bachmair. Canonical Equational Proofs. Progress in Theoret-
ical Computer Science. Birkh¨auser, 1991.
[
Baumgartner and Br¨uning, 1997
]
Peter Baumgartner and Stefan Br¨uning. A Dis-
junctive Positive Refinement of Model Elimination and its Application to Sub-
sumption Deletion. Journal of Automated Reasoning, 19(2):205–262, 1997.
[
Baumgartner and Furbach, 1993
]
P. Baumgartner and U. Furbach. Consolution
as a Framework for Comparing Calculi. Journal of Symbolic Computation,
16(5):445–477, 1993. Academic Press.
[
Baumgartner and Furbach, 1994a
]
P. Baumgartner and U. Furbach. Model Elim-
ination without Contrapositives and its Application to PTTP. Journal of Auto-
mated Reasoning, 13:339–359, 1994. Short version in: Proceedings of CADE-12,
Springer LNAI 814, 1994, pp 87–101.
[
Baumgartner and Furbach, 1994b
]
P. Baumgartner and U. Furbach. Model Elim-
ination without Contrapositives. In A. Bundy, editor, ’Automated Deduction –
CADE-12’, volume 814 of LNAI, pages 87–101. Springer, 1994.
[
Baumgartner and Furbach, 1994c
]
P. Baumgartner and U. Furbach. PRO-
TEIN: A PROver with a T heory Extension I nterface. In A. Bundy,
editor, Automated Deduction – CADE-12, volume 814 of LNAI,
pages 769–773. Springer, 1994. Available in the WWW, URL:
http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/.
[
Baumgartner and Petermann, 1998
]
Peter Baumgartner and Uwe Petermann.
Theory Reasoning. In Bibel and Schmitt
[
1998
]
.
[
Baumgartner and Stolzenburg, 1995
]
P. Baumgartner and F. Stolzenburg. Con-
straint Model Elimination and a PTTP-Implementation. In R. H¨ahnle P. Baum-
gartner and J. Posegga, editors, Theorem Proving with Analytic Tableaux and
Related Methods, volume 918 of Lecture Notes in Artificial Intelligence, pages
201–216, 1995.
[
Baumgartner et al., 1992
]
P. Baumgartner, U. Furbach, and U. Petermann. A
Unified Approach to Theory Reasoning. Research Report 15/92, University of
Koblenz, 1992.
[
Baumgartner et al., 1995
]
P. Baumgartner, U. Furbach, and F. Stolzenburg.
Model Elimination, Logic Programming and Computing Answers. In 14th In-
ternational Joint Conference on Artificial Intelligence (IJCAI 95), volume 1,
1995.
[
Baumgartner et al., 1996
]
P. Baumgartner, U. Furbach, and I. Niemel¨a. Hyper
Tableaux. In Proc. JELIA 96, number 1126 in LNAI. European Workshop on
Logic in AI, Springer, 1996. (Long version in: Fachberichte Informatik, 8–96,
Universit¨at Koblenz-Landau).
[
Baumgartner et al., 1997
]
Peter Baumgartner, Peter Fr¨ohlich, Ulrich Furbach, and
Wolfgang Nejdl. Semantically Guided Theorem Proving for Diagnosis Applica-
tions. In Proc. of IJCAI ’97. IJCAI, 1997.
[
Baumgartner, 1990
]
P. Baumgartner. Combining Horn Clause Logic with Rewrite
Rules. In V. Sgurev Ph. Jorrand, editor, Artificial Intelligence IV – Methodology,
Systems, Applications. Norh Holland, 1990.
[
Baumgartner, 1991a
]
P. Baumgartner. A Completeness Proof Technique for Res-
olution with Equality. In Th. Christaller, editor, GWAI ’91 – 15. Fachtagung
f¨ur K¨unstliche Intelligenz, pages 12–22. Springer, 1991. Informatik Fachberichte
285.
[
Baumgartner, 1991b
]
P. Baumgartner. A Model Elimination Calculus with Built-
in Theories. Fachbericht Informatik 7/91, Universit¨at Koblenz, 1991.
[
Baumgartner, 1992a
]
P. Baumgartner. A Model Elimination Calculus with Built-
in Theories. In H.-J. Ohlbach, editor, Proceedings of the 16-th German AI-
Conference (GWAI-92), pages 30–42. Springer, 1992. LNAI 671.
Bibliography 271
[
Baumgartner, 1992b
]
P. Baumgartner. An Ordered Theory Resolution Calculus.
In A. Voronkov, editor, Logic Programming and Automated Reasoning (Pro-
ceedings), pages 119–130, St. Petersburg, Russia, July 1992. Springer. LNAI
624.
[
Baumgartner, 1993
]
P. Baumgartner. Refinements of Theory Model Elimination
and a Variant without Contrapositives. Research Report 8/93, University of
Koblenz, 1993. (Short version in Proc. ECAI 94, 1994, Wiley).
[
Baumgartner, 1994
]
P. Baumgartner. Refinements of Theory Model Elimination
and a Variant without Contrapositives. In A.G. Cohn, editor, 11th European
Conference on Artificial Intelligence, ECAI 94. Wiley, 1994.
[
Baumgartner, 1996
]
Peter Baumgartner. Linear and Unit-Resulting Refutations
for Horn Theories. Journal of Automated Reasoning, 16(3):241–319, June 1996.
[
Beckert and H¨ahnle, 1992
]
B. Beckert and R. H¨ahnle. An Improved Method for
Adding Equality to Free Variable semantic Tableaux. In D. Kapur, editor, 11th
International Conference on Automated Deduction, volume 607 of LNCS, pages
507–521. Springer, 1992.
[
Beckert and Pape, 1996
]
B. Beckert and C. Pape. Incremental Theory Reasoning
Methods for Semantic Tableaux. In Theorem Proving with Analytic Tableaux
and Related Methods (Tableaux 96). Springer, 1996.
[
Beckert et al., 1996
]
Bernhard Beckert, Reiner H¨ahnle, Peter Oel, and Martin
Sulzmann. The tableau-based theorem prover
3
T
A
P , version 4.0. In M.A.
McRobbie and J.K. Slaney, editors, Automated Deduction — CADE 13, LNAI
1104, pages 303–307, New Brunswick, NJ, USA, July 1996. Springer-Verlag.
[
Beckert, 1994
]
B. Beckert. A completion-based method for mixed universal and
rigid E-unification. In Bundy
[
1994
]
, pages 678–692.
[
Beckert, 1998
]
Bernhard Beckert. Equality and other theory inferences. In
D’Agostino et al.
[
1998
]
.
[
Benanav, 1990
]
Dan Benanav. Simultaneous paramodulation. In Stickel
[
1990b
]
,
pages 442–455.
[
Bertling, 1990
]
Hubert Bertling. Knuth-Bendix Completion of Horn Clause Pro-
grams for Restricted Linear Resolution and Paramodulation. In S. Kaplan and
M. Okada, editors, Proceedings of the 2nd International Workshop on Condi-
tional and Typed Rewriting Systems, pages 181–193. Springer-Verlag, June 1990.
LNCS 516.
[
Bibel and Schmitt, 1998
]
Wolfgang Bibel and Peter H. Schmitt, editors. Auto-
mated Deduction. A basis for applications. Kluwer Academic Publishers, 1998.
[
Bibel et al., 1994
]
Wolfgang Bibel, Stefan Br¨uning, Uwe Egly, and Thomas Rath.
Komet. In Bundy
[
1994
]
, pages 783–787.
[
Bibel, 1981
]
Wolfgang Bibel. On Matrices with Connections. Journal of the As-
sociation for Computing Machinery, 28:633–645, 1981.
[
Bibel, 1982a
]
W. Bibel. Automated Theorem Proving. Vieweg, 1982.
[
Bibel, 1982b
]
Wolfgang Bibel. A Comparative Study of Several Proof Procedures.
Artificial Intelligence, 18:269–293, 1982.
[
Bibel, 1983
]
Wolfgang Bibel. Matings in Matrices. Communications of the Asso-
ciation for Computing Machinery, 26:844–852, 1983.
[
Bibel, 1987
]
W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.
[
Bibel, 1992
]
W. Bibel. Deduktion, volume 6.2 of Handbuch der Informatik. Old-
enburg, 1992.
[
Bollinger, 1991
]
T. Bollinger. A Model Elimination Calculus for Generalized
Clauses. In IJCAI, 1991.
[
Bonacina and Hsiang, 1992
]
Maria Paola Bonacina and Jieh Hsiang. Incomplete-
ness of the RUE/NRF inference systems. Newsletter of the Association for
Automated Reasoning, No. 20, pages 9–12, May 1992.
272 Bibliography
[
Bonacina and Hsiang, 1994
]
Maria Paola Bonacina and Jieh Hsiang. Paralleliza-
tion of deduction strategies: an analytical study. Journal of Automated Reason-
ing, 13:1–33, 1994.
[
Bonacina and Hsiang, 1995
]
Maria Paola Bonacina and Jieh Hsiang. Towards a
foundation of completion procedures as semidecision procedures. Theoretical
Computer Science, 146:199–242, July 1995.
[
Brachman and Schmolze, 1985
]
Ronald J. Brachman and J. G. Schmolze. An
overview of the KL-ONE knowledge representation system. Cognitive Science,
9(2):171–216, 1985.
[
Brachmann et al., 1983
]
R. Brachmann, R. Fikes, and H. Levesque. KRYPTON: a
functional approach to knowledge representation. IEEE Computer, 16(10):67–
73, October 1983.
[
Brand, 1975
]
D. Brand. Proving theorems with the modification method. SIAM
Journal on Computing, 4:412–430, 1975.
[
Bronsard and Reddy, 1992
]
Francois Bronsard and Uday S. Reddy. Reduction
Techniques for First-Order Reasoning. In M. Rusinowitch and J.L. R´emy, ed-
itors, Proceedings of the Third International Workshop on Conditional Term
Rewriting Systems, pages 242–256. Springer-Verlag, July 1992. LNCS 656.
[
Brown, 1978
]
Frank Malloy Brown. Towards the automation of set theory and its
logic. Artificial Intelligence, 10(3):281–316, 1978.
[
Br¨uning, 1995
]
S. Br¨uning. Exploiting Equivalences in Connection Calculi. Jour-
nal of the IGPL, 3(6):857–886, 1995.
[
Bundy, 1994
]
Alan Bundy, editor. Automated Deduction — CADE 12, LNAI 814,
Nancy, France, June 1994. Springer-Verlag.
[
B¨urckert, 1990
]
H.J. B¨urckert. A Resolution Principle for Clauses with Con-
straints. In Stickel
[
1990b
]
, pages 178–192.
[
B¨urckert, 1991
]
H.-J. B¨urckert. A Resolution Principle for Clauses with Restricted
Quantifiers, volume 568 of LNAI. Springer, 1991.
[
B¨uttner, 1986
]
W. B¨uttner. Unification in the Datastructure Multisets. Journal
of Automated Reasoning, 2:75–88, 1986.
[
Chang and Lee, 1973
]
C. Chang and R. Lee. Symbolic Logic and Mechanical The-
orem Proving. Academic Press, 1973.
[
Christoph Goller and Schumann, 1994
]
Klaus Mayr Christoph Goller, Rein-
hold Letz and Johann Schumann. Setheo v3.2: Recent developments — system
abstract —. In Bundy
[
1994
]
, pages 778–782.
[
Chu and Plaisted, 1994
]
Heng Chu and David A. Plaisted. Semantically Guided
First-Order Theorem Proving using Hyper-Linking. In Bundy
[
1994
]
, pages
192–206.
[
D’Agostino et al., 1998
]
Marcello D’Agostino, Dov Gabbay, Reiner H¨ahnle, and
Joachim Posegga, editors. Handbook of Tableau Methods. Kluwer, Dordrecht,
1998.
[
Davis and Putnam, 1960
]
M. Davis and H. Putnam. A Computing Procedure for
Quantification Theory. Journal of the ACM, 7:201–215, 1960.
[
de Kogel, 1995
]
E. de Kogel. Rigid E-unification simplified. In R. H¨ahnle P. Baum-
gartner and J. Posegga, editors, Theorem Proving with Analytic Tableaux and
Related Methods, volume 918 of Lecture Notes in Artificial Intelligence, pages
17–30, 1995.
[
Degtyarev and Voronkov, 1995a
]
A. Degtyarev and A. Voronkov. Equality Elimi-
nation for the Inverse Method and Extension Procedures. In C.S. Mellish, editor,
IJCAI 95: 14th International Conference on Artificial Intelligence, 1995.
[
Degtyarev and Voronkov, 1995b
]
A. Degtyarev and A. Voronkov. Simultaneous
Rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala
University, 1995.
Bibliography 273
[
Dershowitz and Manna, 1979
]
N. Dershowitz and Z. Manna. Proving Termination
with multiset orderings. Comm. ACM, 22:465–476, 1979.
[
Dershowitz and Sivakumar, 1988
]
Nachum Dershowitz and G. Sivakumar. Goal-
Directed Equation Solving. In Proceedings of the AAAI-88, 1988.
[
Dershowitz, 1982
]
N. Dershowitz. Orderings for Term-Rewriting Systems. Theo-
retical Computer Science, 17:279–301, 1982.
[
Dershowitz, 1985
]
N. Dershowitz. Computing with Rewrite Systems. Information
and Control, 65:122 – 157, 1985.
[
Dershowitz, 1987
]
Nachum Dershowitz. Termination of Rewriting. Journal of
Symbolic Computation, 3(1&2):69–116, February/April 1987.
[
Dershowitz, 1990
]
Nachum Dershowitz. A Maximal-Literal Unit Strategy for Horn
Clauses. In S. Kaplan and M. Okada, editors, Proceedings of the 2nd Interna-
tional Workshop on Conditional and Typed Rewriting Systems, pages 14–25.
Springer-Verlag, June 1990. LNCS 516.
[
Dershowitz, 1991a
]
N. Dershowitz. Ordering-Based Strategies for Horn Clauses.
In Proc. IJCAI, 1991.
[
Dershowitz, 1991b
]
Nachum Dershowitz. Canonical Sets of Horn Clauses. In J.
Leach Albert, B. Monien, and M. Rodr´ıguez Artalejo, editors, Proceedings of
the 18th International Colloquium on Automata, Languages and Programming,
pages 267–278, July 1991. LNCS 510.
[
Digricoli and Harrison, 1986
]
Vincent J. Digricoli and Malcolm C. Harrison.
Equality-Based binary Resolution. Journal of the Association for Computing
Machinery, 1986.
[
Dixon, 1973
]
J. Dixon. Z-Resolution: Theorem-Proving with Compiled Axioms.
Journal of the ACM, 20(1):127–147, 1973.
[
Eder, 1991
]
E. Eder. Consolution and its Relation with Resolution. In Proc. IJCAI
’91, 1991.
[
Eder, 1992
]
E. Eder. Relative Complexities of First Order Languages. Vieweg,
1992.
[
Enderton, 1972
]
H.B. Enderton. A Mathematical Introduction to Logic. Academic
Press, 1972.
[
Fages and Huet, 1986
]
F. Fages and G. Huet. Complete Sets of Unifiers and
Matchers in Equational Theories. Theoretical Computer Science, 43, 1986.
[
Fages, 1984
]
F. Fages. Associative-commutative unification. Rapports de
Recherche 287, INRIA, April 1984.
[
Fitting, 1990
]
M. Fitting. First Order Logic and Automated Theorem Proving.
Texts and Monographs in Computer Science. Springer, 1990.
[
Fitting, 1993
]
Melvin Fitting. Basic Modal Logic. In Gabbay et al.
[
1993
]
, pages
365–448.
[
Frisch, 1991
]
A. M. Frisch. The Substitutional Framework for Sorted Deduction:
Fundamental Results on Hybrid Reasoning. Artificial Intelligence, 49:161–198,
1991.
[
Furbach et al., 1989a
]
U. Furbach, S. H¨olldobler, and J. Schreiber. Horn Equa-
tional Theories and Paramodulation. Journal of Automated Reasoning, 5:309–
337, 1989.
[
Furbach et al., 1989b
]
U. Furbach, S. H¨olldobler, and J. Schreiber. Paramodula-
tion modulo equality. In Proc. GWAI’89, pages 107–116. Springer, IFB 216,
1989.
[
Furbach et al., 1989c
]
Ulrich Furbach, Steffen H¨olldobler, and Joachim Schreiber.
Horn equational theories and paramodulation. Journal of Automated Reasoning,
3:309–337, 1989.
[
Furbach, 1991
]
U. Furbach. Logische und Funktionale Programmierung — Grund-
lagen einer Kombination.K¨unstliche Intelligenz. Vieweg, 1991.
274 Bibliography
[
Gabbay et al., 1993
]
Dov M. Gabbay, C.J. Hogger, and J.A. Robinson, editors.
Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 1:
Logical Foundations. Oxford Science Publications, 1993.
[
Gallier and Snyder, 1990
]
J. Gallier and W. Snyder. Designing Unification Proce-
dures Using Transformations: A Survey. Bulletin of the EATCS, 40:273 – 326,
1990.
[
Gallier et al., 1987
]
J. H. Gallier, S. Raatz, and W. Snyder. Theorem proving
using rigid e-unification: Equational matings. In Logics in Computer Science
’87, Ithaca, New York, 1987.
[
Gallier et al., 1992
]
Jean Gallier, Paliath Narendran, Stan Raatz, and Wayne Sny-
der. Theorem Proving Using Equational Matings and Rigid E-Unification. Jour-
nal of the ACM, 39(2):377–429, April 1992.
[
Gallier, 1987
]
J. Gallier. Logic for Computer Science: Foundations of Automatic
Theorem Proving. Wiley, 1987.
[
Ganzinger, 1991
]
Harald Ganzinger. A Completion Procedure for Conditional
Equations. Journal of Symbolic Computation, 11:51–81, 1991.
[
Gentzen, 1939
]
Gerhard Gentzen. Untersuchungen ¨uber das logische Schließen.
Mathematische Zeitschrift, 176–210, 405–431, 1939. English translation in: Sz-
abo, M. (ed.), The Collected Papers of Gerhard Gentzen, pp. 68–131, North
Holland, Amsterdam, 1969.
[
Hanschke and Hinkelmann, 1992
]
P. Hanschke and K. Hinkelmann. Combining
Terminological and Rule-based Reasoning for Abstraction Processes. In H.-J.
Ohlbach, editor, Proceedings of the 16-th German AI-Conference (GWAI-92),
pages 144–155. Springer, 1992. LNAI 671.
[
Heinemann and Weihrauch, 1991
]
B. Heinemann and K. Weihrauch. Logik f¨ur
Informatiker. Leitf¨aden und Monographien der Informatik. B.G. Teubner, 1991.
(in German).
[
Hines, 1990
]
L. Hines. Str+ve⊆: The Str+ve-based Subset Prover. In Stickel
[
1990b
]
, pages 193–206.
[
Hines, 1992
]
L. Hines. The Central Variable Strategy of Str
˙
+ve. In Kapur
[
1992
]
,
pages 35–49.
[
H¨olldobler, 1989
]
Steffen H¨olldobler. Foundations of Equational Logic Program-
ming, volume 353 of Lecture Notes in Artificial Intelligence. Subseries of Lecture
Notes in Computer Science. Springer, 1989.
[
Hollunder, 1990
]
B. Hollunder. Hybrid Inferences in KL-ONE-based Knowledge
Representation Systems. Research Report RR-90-6, DFKI, May 1990.
[
Hopcroft and Ullman, 1979
]
A. Hopcroft and D. Ullman. Formal languages and
their relation to automata. Addison-Wesley, 1979.
[
Hsiang and Rusinowitch, 1986
]
J. Hsiang and M. Rusinowitch. A New Method for
Establishing Refutational Completeness in Theorem Proving. In J¨org Siekmann,
editor, 8th International Conference on Automated Deduction, LNCS 230, pages
141–152, Oxford, England, 1986. Springer-Verlag.
[
Hsiang and Rusinowitch, 1987
]
J. Hsiang and M. Rusinowitch. On word problems
in equational theories. In Proc. ICALP’87, pages 54–71. Springer, LNCS 267,
1987.
[
Hsiang and Rusinowitch, 1991
]
Jieh Hsiang and Mich¨ael Rusinowitch. Proving
refutational completeness of theorem proving strategies: the transfinite semantic
tree method. Journal of the ACM, 38(3):559–587, 1991.
[
Hsiang, 1985
]
J. Hsiang. Refutational theorem proving using term rewriting sys-
tems. Artificial Intelligence, 25:255–300, 1985.
[
Huet and Oppen, 1980
]
G´erard Huet and Derek C. Oppen. Equations and Rewrite
Rules. A Survey. In R. Book, editor, Formal Languages: Perspectives and Open
Problems, pages 349–405. Academic Press, 1980.