The applicability of logic program analysis and transformation to theorem proving

D. A. de Waal; John Patrick Gallagher

doi:10.1007/3-540-58156-1_15

The applicability of logic program analysis and transformation to theorem proving

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Abstract

Analysis and transformation techniques developed for logic programming can be successfully applied to automatic theorem proving. In this paper we demonstrate how these techniques can prune the search space of the theorem prover, by detecting inference rules and clauses that cannot contribute to proofs. The specialisation techniques developed in this paper are applied to first order clausal theorem provers, but are independent of the logic and the proof system and can therefore be applied to all theorem provers written as logic programs.

Originalsprog	Engelsk
Titel	Automated Deduction - CADE-12 : 12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings
Redaktører	Alan Bundy
Udgivelsessted	Berlin
Forlag	Springer Verlag
Publikationsdato	1994
Sider	207-221
ISBN (Trykt)	978-3-540-58156-7
ISBN (Elektronisk)	978-3-540-48467-7
DOI	https://doi.org/10.1007/3-540-58156-1_15
Status	Udgivet - 1994
Udgivet eksternt	Ja
Begivenhed	12th International Conference on Automated Deduction, CADE-12 1994 - Nancy, Frankrig Varighed: 26 jun. 1994 → 1 jul. 1994

Konference

Konference	12th International Conference on Automated Deduction, CADE-12 1994
Land/Område	Frankrig
By	Nancy
Periode	26/06/1994 → 01/07/1994
Sponsor	Cade General Contractors

Navn	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind	814 LNAI
ISSN	0302-9743

Bibliografisk note

Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1994.

Link til dokument

10.1007/3-540-58156-1_15

Citer dette

de Waal, D. A. ; Gallagher, John Patrick. / The applicability of logic program analysis and transformation to theorem proving. Automated Deduction - CADE-12: 12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings. red. / Alan Bundy. Berlin : Springer Verlag, 1994. s. 207-221 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 814 LNAI).

@inproceedings{8b58f783ab0746b5b9af1a86da73b057,

title = "The applicability of logic program analysis and transformation to theorem proving",

abstract = "Analysis and transformation techniques developed for logic programming can be successfully applied to automatic theorem proving. In this paper we demonstrate how these techniques can prune the search space of the theorem prover, by detecting inference rules and clauses that cannot contribute to proofs. The specialisation techniques developed in this paper are applied to first order clausal theorem provers, but are independent of the logic and the proof system and can therefore be applied to all theorem provers written as logic programs.",

author = "{de Waal}, {D. A.} and Gallagher, {John Patrick}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1994.; 12th International Conference on Automated Deduction, CADE-12 1994 ; Conference date: 26-06-1994 Through 01-07-1994",

year = "1994",

doi = "10.1007/3-540-58156-1_15",

language = "English",

isbn = "978-3-540-58156-7",

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

publisher = "Springer Verlag",

pages = "207--221",

editor = "Alan Bundy",

booktitle = "Automated Deduction - CADE-12",

}

de Waal, DA & Gallagher, JP 1994, The applicability of logic program analysis and transformation to theorem proving. i A Bundy (red.), Automated Deduction - CADE-12: 12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings. Springer Verlag, Berlin, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 814 LNAI, s. 207-221, 12th International Conference on Automated Deduction, CADE-12 1994, Nancy, Frankrig, 26/06/1994. https://doi.org/10.1007/3-540-58156-1_15

The applicability of logic program analysis and transformation to theorem proving. / de Waal, D. A.; Gallagher, John Patrick.
Automated Deduction - CADE-12: 12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings. red. / Alan Bundy. Berlin: Springer Verlag, 1994. s. 207-221 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 814 LNAI).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - The applicability of logic program analysis and transformation to theorem proving

AU - de Waal, D. A.

AU - Gallagher, John Patrick

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1994.

PY - 1994

Y1 - 1994

N2 - Analysis and transformation techniques developed for logic programming can be successfully applied to automatic theorem proving. In this paper we demonstrate how these techniques can prune the search space of the theorem prover, by detecting inference rules and clauses that cannot contribute to proofs. The specialisation techniques developed in this paper are applied to first order clausal theorem provers, but are independent of the logic and the proof system and can therefore be applied to all theorem provers written as logic programs.

AB - Analysis and transformation techniques developed for logic programming can be successfully applied to automatic theorem proving. In this paper we demonstrate how these techniques can prune the search space of the theorem prover, by detecting inference rules and clauses that cannot contribute to proofs. The specialisation techniques developed in this paper are applied to first order clausal theorem provers, but are independent of the logic and the proof system and can therefore be applied to all theorem provers written as logic programs.

U2 - 10.1007/3-540-58156-1_15

DO - 10.1007/3-540-58156-1_15

M3 - Article in proceedings

AN - SCOPUS:0342295077

SN - 978-3-540-58156-7

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

SP - 207

EP - 221

BT - Automated Deduction - CADE-12

A2 - Bundy, Alan

PB - Springer Verlag

CY - Berlin

T2 - 12th International Conference on Automated Deduction, CADE-12 1994

Y2 - 26 June 1994 through 1 July 1994

ER -

de Waal DA, Gallagher JP. The applicability of logic program analysis and transformation to theorem proving. I Bundy A, red., Automated Deduction - CADE-12: 12th International Conference on Automated Deduction Nancy, France, June 26–July 1, 1994 Proceedings. Berlin: Springer Verlag. 1994. s. 207-221. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 814 LNAI). doi: 10.1007/3-540-58156-1_15