Hyperparamodulation

A refinement of paramodulation

L. Wos, R. Overbeek, Lawrence Joseph Henschen

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

9 Citations (Scopus)

Abstract

A refinement of paramodulation, called hyperparamodulation, is the focus of attention in this paper. Clauses obtained by the use of this inference rule are, in effect, the result of a sequence of paramodulations into one coranon nucleus. Among the interesting properties of hyperparamodulation are: first, clauses are chosen from among the input and designated as nuclei or "into" clauses for paramodulation; second, terms in the nucleus are starred to restrict the domain of generalized equality substitution; third, total control is thus iteratively established over all possible targets for paramodulation during the entire run of the theorem-proving program; and fourth, application of demodulation is suspended until the hyperparamodulant is completed. In contrast to these four properties which are reminiscent of the spirit of hyper-resolution, the following differences exist: first, the nucleus and the starred terms therein, which are analogous to negative literals, are determined by the user rather than by syntax; second, nuclei are not restricted to being mixed clauses; and third, while hyper-resolution requires inferred clauses to be positive, no corresponding requirement exists for clauses inferred by hyperparamodulation. To illustrate the value of this refinement of paramodulation, we have chosen certain conjectures which arose during the study of Robbins algebra. A Robbins algebra is a set on which the functions o and n are defined such that o is both commutative and associative and such that for all x and y the following identity n(o(n(o(x,y)),n(o(x,n(y))))) =x holds. One may think of o as union and n as complement. Hie main interest in such algebras arises from the following open question: If S is a Robbins algebra, is S necessarily a Boolean algebra? The study of this open question entailed heavy use of an automated theorem-proving program to examine various conjectures. Certain computer proofs therein were obtained only after recourse to hyperparamodulation. (These lenmas were actually obtained prior to the work reported on here by Winker and Wos using a non-standard theorem-proving approach developed by Winker.).

Original languageEnglish (US)
Title of host publication5th Conference on Automated Deduction
EditorsWolfgang Bibel, Robert Kowalski
PublisherSpringer Verlag
Pages208-219
Number of pages12
ISBN (Print)9783540100096
StatePublished - Jan 1 1980
Event5th International Conference on Automated Deduction, CADE 1980 - Les Arcs, France
Duration: Jul 8 1980Jul 11 1980

Publication series

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

Other

Other5th International Conference on Automated Deduction, CADE 1980
CountryFrance
CityLes Arcs
Period7/8/807/11/80

Fingerprint

Theorem proving
Algebra
Nucleus
Refinement
Theorem Proving
Boolean algebra
Automated Theorem Proving
Demodulation
Set theory
Inference Rules
Term
Substitution reactions
Substitution
Equality
Union
Complement
Entire
Target
Requirements

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Wos, L., Overbeek, R., & Henschen, L. J. (1980). Hyperparamodulation: A refinement of paramodulation. In W. Bibel, & R. Kowalski (Eds.), 5th Conference on Automated Deduction (pp. 208-219). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 87 LNCS). Springer Verlag.
Wos, L. ; Overbeek, R. ; Henschen, Lawrence Joseph. / Hyperparamodulation : A refinement of paramodulation. 5th Conference on Automated Deduction. editor / Wolfgang Bibel ; Robert Kowalski. Springer Verlag, 1980. pp. 208-219 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{353141bc247b4ec7b1078e372ac06757,
title = "Hyperparamodulation: A refinement of paramodulation",
abstract = "A refinement of paramodulation, called hyperparamodulation, is the focus of attention in this paper. Clauses obtained by the use of this inference rule are, in effect, the result of a sequence of paramodulations into one coranon nucleus. Among the interesting properties of hyperparamodulation are: first, clauses are chosen from among the input and designated as nuclei or {"}into{"} clauses for paramodulation; second, terms in the nucleus are starred to restrict the domain of generalized equality substitution; third, total control is thus iteratively established over all possible targets for paramodulation during the entire run of the theorem-proving program; and fourth, application of demodulation is suspended until the hyperparamodulant is completed. In contrast to these four properties which are reminiscent of the spirit of hyper-resolution, the following differences exist: first, the nucleus and the starred terms therein, which are analogous to negative literals, are determined by the user rather than by syntax; second, nuclei are not restricted to being mixed clauses; and third, while hyper-resolution requires inferred clauses to be positive, no corresponding requirement exists for clauses inferred by hyperparamodulation. To illustrate the value of this refinement of paramodulation, we have chosen certain conjectures which arose during the study of Robbins algebra. A Robbins algebra is a set on which the functions o and n are defined such that o is both commutative and associative and such that for all x and y the following identity n(o(n(o(x,y)),n(o(x,n(y))))) =x holds. One may think of o as union and n as complement. Hie main interest in such algebras arises from the following open question: If S is a Robbins algebra, is S necessarily a Boolean algebra? The study of this open question entailed heavy use of an automated theorem-proving program to examine various conjectures. Certain computer proofs therein were obtained only after recourse to hyperparamodulation. (These lenmas were actually obtained prior to the work reported on here by Winker and Wos using a non-standard theorem-proving approach developed by Winker.).",
author = "L. Wos and R. Overbeek and Henschen, {Lawrence Joseph}",
year = "1980",
month = "1",
day = "1",
language = "English (US)",
isbn = "9783540100096",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "208--219",
editor = "Wolfgang Bibel and Robert Kowalski",
booktitle = "5th Conference on Automated Deduction",
address = "Germany",

}

Wos, L, Overbeek, R & Henschen, LJ 1980, Hyperparamodulation: A refinement of paramodulation. in W Bibel & R Kowalski (eds), 5th Conference on Automated Deduction. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 87 LNCS, Springer Verlag, pp. 208-219, 5th International Conference on Automated Deduction, CADE 1980, Les Arcs, France, 7/8/80.

Hyperparamodulation : A refinement of paramodulation. / Wos, L.; Overbeek, R.; Henschen, Lawrence Joseph.

5th Conference on Automated Deduction. ed. / Wolfgang Bibel; Robert Kowalski. Springer Verlag, 1980. p. 208-219 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 87 LNCS).

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

TY - GEN

T1 - Hyperparamodulation

T2 - A refinement of paramodulation

AU - Wos, L.

AU - Overbeek, R.

AU - Henschen, Lawrence Joseph

PY - 1980/1/1

Y1 - 1980/1/1

N2 - A refinement of paramodulation, called hyperparamodulation, is the focus of attention in this paper. Clauses obtained by the use of this inference rule are, in effect, the result of a sequence of paramodulations into one coranon nucleus. Among the interesting properties of hyperparamodulation are: first, clauses are chosen from among the input and designated as nuclei or "into" clauses for paramodulation; second, terms in the nucleus are starred to restrict the domain of generalized equality substitution; third, total control is thus iteratively established over all possible targets for paramodulation during the entire run of the theorem-proving program; and fourth, application of demodulation is suspended until the hyperparamodulant is completed. In contrast to these four properties which are reminiscent of the spirit of hyper-resolution, the following differences exist: first, the nucleus and the starred terms therein, which are analogous to negative literals, are determined by the user rather than by syntax; second, nuclei are not restricted to being mixed clauses; and third, while hyper-resolution requires inferred clauses to be positive, no corresponding requirement exists for clauses inferred by hyperparamodulation. To illustrate the value of this refinement of paramodulation, we have chosen certain conjectures which arose during the study of Robbins algebra. A Robbins algebra is a set on which the functions o and n are defined such that o is both commutative and associative and such that for all x and y the following identity n(o(n(o(x,y)),n(o(x,n(y))))) =x holds. One may think of o as union and n as complement. Hie main interest in such algebras arises from the following open question: If S is a Robbins algebra, is S necessarily a Boolean algebra? The study of this open question entailed heavy use of an automated theorem-proving program to examine various conjectures. Certain computer proofs therein were obtained only after recourse to hyperparamodulation. (These lenmas were actually obtained prior to the work reported on here by Winker and Wos using a non-standard theorem-proving approach developed by Winker.).

AB - A refinement of paramodulation, called hyperparamodulation, is the focus of attention in this paper. Clauses obtained by the use of this inference rule are, in effect, the result of a sequence of paramodulations into one coranon nucleus. Among the interesting properties of hyperparamodulation are: first, clauses are chosen from among the input and designated as nuclei or "into" clauses for paramodulation; second, terms in the nucleus are starred to restrict the domain of generalized equality substitution; third, total control is thus iteratively established over all possible targets for paramodulation during the entire run of the theorem-proving program; and fourth, application of demodulation is suspended until the hyperparamodulant is completed. In contrast to these four properties which are reminiscent of the spirit of hyper-resolution, the following differences exist: first, the nucleus and the starred terms therein, which are analogous to negative literals, are determined by the user rather than by syntax; second, nuclei are not restricted to being mixed clauses; and third, while hyper-resolution requires inferred clauses to be positive, no corresponding requirement exists for clauses inferred by hyperparamodulation. To illustrate the value of this refinement of paramodulation, we have chosen certain conjectures which arose during the study of Robbins algebra. A Robbins algebra is a set on which the functions o and n are defined such that o is both commutative and associative and such that for all x and y the following identity n(o(n(o(x,y)),n(o(x,n(y))))) =x holds. One may think of o as union and n as complement. Hie main interest in such algebras arises from the following open question: If S is a Robbins algebra, is S necessarily a Boolean algebra? The study of this open question entailed heavy use of an automated theorem-proving program to examine various conjectures. Certain computer proofs therein were obtained only after recourse to hyperparamodulation. (These lenmas were actually obtained prior to the work reported on here by Winker and Wos using a non-standard theorem-proving approach developed by Winker.).

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

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

M3 - Conference contribution

SN - 9783540100096

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

SP - 208

EP - 219

BT - 5th Conference on Automated Deduction

A2 - Bibel, Wolfgang

A2 - Kowalski, Robert

PB - Springer Verlag

ER -

Wos L, Overbeek R, Henschen LJ. Hyperparamodulation: A refinement of paramodulation. In Bibel W, Kowalski R, editors, 5th Conference on Automated Deduction. Springer Verlag. 1980. p. 208-219. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).