Internal analogy in theorem proving

Erica Melis; Jon Whittle

doi:10.1007/3-540-61511-3_71

Internal analogy in theorem proving

Erica Melis, Jon Whittle

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

6 Citations (Scopus)

Abstract

Internal analogy tries to reuse solutions of subproblems within the same problem solving process. In mathematical theorem proving several patterns are known where internal analogy suggests itself. Hence, we propose the use of internal analogy in automated theorem proving. This paper investigates the possibility of incorporating internal analogy into the inductive proof planner CL^AM. It introduces internal analogy as a control strategy of CL^AM that can reduce search. We concentrate on using internal analogy to avoid the repeated application of the induction revision critic. The implementation has been tested and it was found that internal analogy can reduce the time taken to construct proof plans for some theorems.

Original language	English
Title of host publication	Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings
Editors	John K. Slaney, Michael A. McRobbie
Publisher	Springer
Pages	92-105
Number of pages	14
ISBN (Print)	3540615113, 9783540615118
DOIs	https://doi.org/10.1007/3-540-61511-3_71
Publication status	Published - 1 Jan 1996
Externally published	Yes
Event	International Conference on Automated Deduction 1996 - New Brunswick, United States of America Duration: 30 Jul 1996 → 3 Aug 1996 Conference number: 13th

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1104
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Automated Deduction 1996
Abbreviated title	CADE 1996
Country/Territory	United States of America
City	New Brunswick
Period	30/07/96 → 3/08/96

Access to Document

10.1007/3-540-61511-3_71

Cite this

Melis, E., & Whittle, J. (1996). Internal analogy in theorem proving. In J. K. Slaney, & M. A. McRobbie (Eds.), Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings (pp. 92-105). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1104). Springer. https://doi.org/10.1007/3-540-61511-3_71

Melis, Erica ; Whittle, Jon. / Internal analogy in theorem proving. Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. editor / John K. Slaney ; Michael A. McRobbie. Springer, 1996. pp. 92-105 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{002de838e8404054ab59d7f6cb3d9ae5,

title = "Internal analogy in theorem proving",

abstract = "Internal analogy tries to reuse solutions of subproblems within the same problem solving process. In mathematical theorem proving several patterns are known where internal analogy suggests itself. Hence, we propose the use of internal analogy in automated theorem proving. This paper investigates the possibility of incorporating internal analogy into the inductive proof planner CLAM. It introduces internal analogy as a control strategy of CLAM that can reduce search. We concentrate on using internal analogy to avoid the repeated application of the induction revision critic. The implementation has been tested and it was found that internal analogy can reduce the time taken to construct proof plans for some theorems.",

author = "Erica Melis and Jon Whittle",

year = "1996",

month = jan,

day = "1",

doi = "10.1007/3-540-61511-3_71",

language = "English",

isbn = "3540615113",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "92--105",

editor = "Slaney, {John K.} and McRobbie, {Michael A.}",

booktitle = "Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings",

note = "International Conference on Automated Deduction 1996, CADE 1996 ; Conference date: 30-07-1996 Through 03-08-1996",

}

Melis, E & Whittle, J 1996, Internal analogy in theorem proving. in JK Slaney & MA McRobbie (eds), Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1104, Springer, pp. 92-105, International Conference on Automated Deduction 1996, New Brunswick, New Jersey, United States of America, 30/07/96. https://doi.org/10.1007/3-540-61511-3_71

Internal analogy in theorem proving. / Melis, Erica; Whittle, Jon.

Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. ed. / John K. Slaney; Michael A. McRobbie. Springer, 1996. p. 92-105 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1104).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Internal analogy in theorem proving

AU - Melis, Erica

AU - Whittle, Jon

N1 - Conference code: 13th

PY - 1996/1/1

Y1 - 1996/1/1

N2 - Internal analogy tries to reuse solutions of subproblems within the same problem solving process. In mathematical theorem proving several patterns are known where internal analogy suggests itself. Hence, we propose the use of internal analogy in automated theorem proving. This paper investigates the possibility of incorporating internal analogy into the inductive proof planner CLAM. It introduces internal analogy as a control strategy of CLAM that can reduce search. We concentrate on using internal analogy to avoid the repeated application of the induction revision critic. The implementation has been tested and it was found that internal analogy can reduce the time taken to construct proof plans for some theorems.

AB - Internal analogy tries to reuse solutions of subproblems within the same problem solving process. In mathematical theorem proving several patterns are known where internal analogy suggests itself. Hence, we propose the use of internal analogy in automated theorem proving. This paper investigates the possibility of incorporating internal analogy into the inductive proof planner CLAM. It introduces internal analogy as a control strategy of CLAM that can reduce search. We concentrate on using internal analogy to avoid the repeated application of the induction revision critic. The implementation has been tested and it was found that internal analogy can reduce the time taken to construct proof plans for some theorems.

UR - http://www.scopus.com/inward/record.url?scp=84957718440&partnerID=8YFLogxK

U2 - 10.1007/3-540-61511-3_71

DO - 10.1007/3-540-61511-3_71

M3 - Conference Paper

AN - SCOPUS:84957718440

SN - 3540615113

SN - 9783540615118

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 92

EP - 105

BT - Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings

A2 - Slaney, John K.

A2 - McRobbie, Michael A.

PB - Springer

T2 - International Conference on Automated Deduction 1996

Y2 - 30 July 1996 through 3 August 1996

ER -

Melis E, Whittle J. Internal analogy in theorem proving. In Slaney JK, McRobbie MA, editors, Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings. Springer. 1996. p. 92-105. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-61511-3_71

Internal analogy in theorem proving

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this