Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
A Short Introduction to Computational Trends in Analogical Reasoning Read chapter Read first chapter

2014 | OriginalPaper | Chapter

Analogy in Automated Deduction: A Survey

Authors : Thierry Boy de la Tour, Nicolas Peltier

Published in: Computational Approaches to Analogical Reasoning: Current Trends

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We provide a survey of the main approaches for analogical reasoning in automated deduction. We start by proposing a general framework for reasoning by analogy based on a constrained sequent calculus in which higher-order variables denote first-order formulæ. Then we briefly review the most successful approaches, ranging from early work in Horn logic to proof reuse in interactive higher-order theorem provers. With the help of many examples, we present the main ideas and basic features of each approach and briefly discuss their common points and differences.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Analogy as an Organizational Principle in the Construction of Large Knowledge-Bases
next chapter Applying Belief Revision to Case-Based Reasoning
Footnotes
1
A multiset is a generalization of sets in which members are allowed to appear more than once.
 
2
Remember that quantification is denoted by function application, for instance the formula \(\forall x\, p(x)\) is represented by \(\forall \lambda x\, p(x)\).
 
3
Of course, such symbols would have to be indexed.
 
Literature
1.
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
2.
Barthe, G., Pons, O.: Type isomorphisms and proof reuse in dependent type theory. In: Honsell, F., Miculan, M. (eds.) FoSSaCS, LNCS, vol. 2030, pp. 57–71. Springer, Berlin (2001)
3.
4.
Bourely, C. Caferra, R., Peltier, N.: A method for building models automatically. Experiments with an extension of OTTER. In: Bundy, A. (ed.) Proceedings of CADE-12, LNAI 814, pp. 72–86. Springer, Berlin (1994)
5.
Bourely, C., Défourneaux, G., Peltier, N.: Building proofs or counterexamples by analogy in a resolution framework. In: Alferes, J.J., Pereira, L.M., Orlowska, E. (eds.) Proceedings of JELIA 96, LNAI, vol. 1126, pp. 34–49. Springer, Berlin (1996)
6.
Boy de la tour, T., Caferra, R.: Proof analogy in interactive theorem proving: a method to express and use it via second order matching. In: Proceedings of the Sixth National Conference on Artificial Intelligence AAAI-87, Morgan Kaufmann, pp. 95–99 (1987)
7.
Boy de la tour, T., Kreitz, C.: Building proofs by analogy via the Curry-Howard isomorphism. In: Voronkov, A. (ed.) Proceedings of the Conference on Logic Programming and Automated Reasoning LPAR’92, LNAI, vol. 624, pp. 202–213. Springer, Berlin (1992)
8.
Bundy, A., van Harmelen, F., Horn, C., Smaill, A.: The Oyster-clam system. In: Proceedings of the 10th International Conference on Automated Deduction, pp. 647–648. Springer, Berlin (1990)
9.
Caferra, R., Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. J Symb Comput 13, 613–641 (1992)CrossRefMATHMathSciNet
10.
11.
Constable, R.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)
12.
Curien, R.: Second order e-matching as a tool for automated theorem proving. In: Filgueiras, M., Damas, L. (eds.) Progress in Artificial Intelligence, LNCS, vol. 727, pp. 242–257. Springer, Berlin (1993)
13.
Curien, R., Qian, Z., Shi, H.: Efficient second-order matching. In: Ganzinger, H. (ed.) Rewriting Techniques and Applications, LNCS, vol. 1103, pp. 317–331. Springer, Berlin (1996)
14.
Défourneaux, G., Bourely, C., Peltier, N.: Semantic generalizations for proving and disproving conjectures by analogy. J Autom Reason 20(1 & 2), 27–45 (1998)CrossRefMATH
15.
Défourneaux, G., Peltier, N.: Analogy and abduction in automated reasoning. In: Pollack, M.E. (ed.) Proceedings of IJCAI’97, 23–29 Aug (1997)
16.
Défourneaux, G., Peltier, N.: Partial matching for analogy discovery in proofs and counter-examples. In: McCune, W. (ed.) Proceedings of CADE 14, LNAI, vol. 1249, July. Springer, Berlin (1997)
17.
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reason. 31(1), 33–72 (2003)
18.
Felty, A.P., Howe, D.J.: Generalization and reuse of tactic proofs. In: Pfenning, F. (ed.) LPAR, LNCS, vol. 822, pp. 1–15. Springer, Berlin (1994)
19.
20.
Hartshorne, C., Weiss, P., Burks, A.: Collected Papers of C.S. Peirce (1930–1958). Harvard University Press, Cambridge
21.
Hegel, G.: Elements of the Philosophy of Right. Cambridge University Press, Cambridge (1991)
22.
Hetzl, S.: A sequent calculus with implicit term representation. In: Dawar, A., Veith, H. (eds.) CSL, LNCS, vol. 6247, pp. 351–365. Springer, Berlin (2010)
23.
Hetzl, S., Leitsch, A., Weller, D.: Towards algorithmic cut-introduction. In: Bjørner, N., Voronkov, A. (eds.) LPAR, LNCS, vol. 7180, pp. 228–242. Springer, Berlin
24.
Johnsen, E.B., Lüth, C.: Theorem reuse by proof term transformation. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs, LNCS, vol. 3223, pp. 152–167. Springer , Berlin (2004)
25.
Kling, R.E.: A paradigm for reasoning by analogy. In: Proceedings of the 2nd International Joint Conference on Artificial Intelligence, IJCAI’71, Morgan Kaufmann, pp. 568–585 (1971)
26.
Leitsch, A.: The resolution calculus. In: Texts in Theoretical Computer Science. Springer, Berlin (1997)
27.
Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans Program Lang Syst 4(2), 258–282 (1982)CrossRefMATH
28.
29.
Munyer, J.: Analogy as a mean of discovery in problem-solving and learning. PhD thesis, University of California, Santa Cruz (1981)
30.
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin (2002)
31.
Owen, S.: Analogy for Automated Reasoning. Academic Press, New York (1990)
32.
Peltier, N.: A general method for using terms schematizations in automated deduction. In: Proceedings of the International Joint Conference on Automated Reasoning (IJCAR’01), LNCS, vol. 2083, pp. 578–593. Springer, Berlin (2001)
33.
Robinson, A., Voronkov A. (eds.): Handbook of Automated Reasoning. North-Holland, New York (2001)
34.
35.
36.
Metadata
Title
Analogy in Automated Deduction: A Survey
Authors
Thierry Boy de la Tour
Nicolas Peltier
Copyright Year
2014
Publisher
Springer Berlin Heidelberg
Book
Computational Approaches to Analogical Reasoning: Current Trends

Print ISBN: 978-3-642-54515-3

Electronic ISBN: 978-3-642-54516-0

Copyright Year: 2014

DOI
https://doi.org/10.1007/978-3-642-54516-0_5

Premium Partner

    Image Credits