A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

One problem that chain format linear deduction systems can suffer from is the necessity of repeating subdeductions when unifiable literals appear in (possibly distinct) centre chains of a deduction. Four mechanisms for avoiding the repetition are: factoring, lemmas, C-literals, and caching. These mechanisms are examined, and it is concluded that lemmas and C-literals are the mechanisms of choice for this task. A correspondance between the lemma and C-literal mechanisms is described, leading to the introduction of two new repetition avoidance mechanisms. Lemmas, C-literals, and the two new mechanisms have been performance tested. It is concluded that the absolute benefit of using any repetition avoidance mechanism is not large (in the test suite used), but that the C-literal and one of the new mechanisms do improve the performance of the host deduction system.

Original languageEnglish (US)
Title of host publicationLogic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings
PublisherSpringer Verlag
Pages321-332
Number of pages12
Volume698 LNAI
ISBN (Print)9783540569442
StatePublished - 1993
Externally publishedYes
Event4th International Conference on Logic Programming and Automated Reasoning, LPAR 1993 - St. Petersburg, Russian Federation
Duration: Jul 13 1993Jul 20 1993

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume698 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Conference on Logic Programming and Automated Reasoning, LPAR 1993
CountryRussian Federation
CitySt. Petersburg
Period7/13/937/20/93

Fingerprint

Deduction
Linear systems
Lemma
Repetition
Factoring
Caching
Distinct

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Sutcliffe, G. (1993). A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems. In Logic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings (Vol. 698 LNAI, pp. 321-332). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 698 LNAI). Springer Verlag.

A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems. / Sutcliffe, Geoffrey.

Logic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings. Vol. 698 LNAI Springer Verlag, 1993. p. 321-332 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 698 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Sutcliffe, G 1993, A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems. in Logic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings. vol. 698 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 698 LNAI, Springer Verlag, pp. 321-332, 4th International Conference on Logic Programming and Automated Reasoning, LPAR 1993, St. Petersburg, Russian Federation, 7/13/93.
Sutcliffe G. A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems. In Logic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings. Vol. 698 LNAI. Springer Verlag. 1993. p. 321-332. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Sutcliffe, Geoffrey. / A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems. Logic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings. Vol. 698 LNAI Springer Verlag, 1993. pp. 321-332 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{71cc8db3237e47279e98f1a45432c78c,
title = "A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems",
abstract = "One problem that chain format linear deduction systems can suffer from is the necessity of repeating subdeductions when unifiable literals appear in (possibly distinct) centre chains of a deduction. Four mechanisms for avoiding the repetition are: factoring, lemmas, C-literals, and caching. These mechanisms are examined, and it is concluded that lemmas and C-literals are the mechanisms of choice for this task. A correspondance between the lemma and C-literal mechanisms is described, leading to the introduction of two new repetition avoidance mechanisms. Lemmas, C-literals, and the two new mechanisms have been performance tested. It is concluded that the absolute benefit of using any repetition avoidance mechanism is not large (in the test suite used), but that the C-literal and one of the new mechanisms do improve the performance of the host deduction system.",
author = "Geoffrey Sutcliffe",
year = "1993",
language = "English (US)",
isbn = "9783540569442",
volume = "698 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "321--332",
booktitle = "Logic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings",

}

TY - GEN

T1 - A comparison of mechanisms for avoiding repetition of subdeductions in chain format linear deduction systems

AU - Sutcliffe, Geoffrey

PY - 1993

Y1 - 1993

N2 - One problem that chain format linear deduction systems can suffer from is the necessity of repeating subdeductions when unifiable literals appear in (possibly distinct) centre chains of a deduction. Four mechanisms for avoiding the repetition are: factoring, lemmas, C-literals, and caching. These mechanisms are examined, and it is concluded that lemmas and C-literals are the mechanisms of choice for this task. A correspondance between the lemma and C-literal mechanisms is described, leading to the introduction of two new repetition avoidance mechanisms. Lemmas, C-literals, and the two new mechanisms have been performance tested. It is concluded that the absolute benefit of using any repetition avoidance mechanism is not large (in the test suite used), but that the C-literal and one of the new mechanisms do improve the performance of the host deduction system.

AB - One problem that chain format linear deduction systems can suffer from is the necessity of repeating subdeductions when unifiable literals appear in (possibly distinct) centre chains of a deduction. Four mechanisms for avoiding the repetition are: factoring, lemmas, C-literals, and caching. These mechanisms are examined, and it is concluded that lemmas and C-literals are the mechanisms of choice for this task. A correspondance between the lemma and C-literal mechanisms is described, leading to the introduction of two new repetition avoidance mechanisms. Lemmas, C-literals, and the two new mechanisms have been performance tested. It is concluded that the absolute benefit of using any repetition avoidance mechanism is not large (in the test suite used), but that the C-literal and one of the new mechanisms do improve the performance of the host deduction system.

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

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

M3 - Conference contribution

AN - SCOPUS:85028926671

SN - 9783540569442

VL - 698 LNAI

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

SP - 321

EP - 332

BT - Logic Programming and Automated Reasoning - 4th International Conference, LPAR 1993, Proceedings

PB - Springer Verlag

ER -