research-article

Free access

Completeness results for e-resolution

Author:

Robert AndersonAuthors Info & Claims

AFIPS '70 (Spring): Proceedings of the May 5-7, 1970, spring joint computer conference

Pages 653 - 656

https://doi.org/10.1145/1476936.1477034

Published: 05 May 1970 Publication History

PDF eReader

Abstract

Since their introduction in 1965, resolution based deductive systems for the first-order predicate calculus have been extensively investigated and utilized by researchers in the field of automatic theorem-proving by computer. Part of this research has been directed at finding techniques for treating the equality relation within the framework of resolution based deductive systems. Perhaps the most natural treatment of equality, introduced so far, is by means of the para-modulation principle which when used in conjunction with resolution forms a complete deductive system for the first-order predicate calculus with equality. A very similar technique for treating equality was introduced and called E-resolution. In fact E-resolution can be viewed as a restricted form of paramodulation and resolution. The purpose of this paper is to define E-resolution in terms of paramodulation and resolution and to prove the completeness of E-resolution and several modifications of E-resolution.

References

[1]

R Anderson W W Bledsoe A linear format for resolution with merging and a new technique for establishing completeness To appear in Journal of the ACM

Digital Library

Google Scholar

[2]

J L Darlington Automatic theorem-proving with equality substitutions and mathematical induction Machine Intelligence Vol 3 B D Michie ed

Google Scholar

[3]

R Kowalski The case for using equality axioms in automatic demonstration A Paper presented at the Symposium on Automatic Demonstration Paris December 16--21 1968

Google Scholar

[4]

J B Morris E-resolution: Extensions of resolution to include the equality relation Proc International Joint Conference on Artificial Intelligence Washington D C May 7--9 1969

Google Scholar

[5]

G A Robinson L Wos Paramodulation and theorem-proving in first-order theories with equality Machine Intelligence Vol 4 B Meltzer and D Michie eds

Google Scholar

[6]

G A Robinson L Wos Completeness of paramodulation Spring 1968 Meeting of Assn for Symbolic Logic---Abstract to appear in Journal Symbolic Logic

Google Scholar

[7]

J A Robinson A machine oriented logic based on the resolution principle Journal of the ACM Vol 12 No 1 pp 23--41 January 1965

Digital Library

Google Scholar

[8]

J A Robinson Automatic deduction with hyper-resolution Int J Computer Math Vol 1 pp 227--234 1965

Google Scholar

[9]

J A Robinson The generalized resolution principle Machine Intelligence Vol 3 D Michie ed

Google Scholar

[10]

E E Sibert A machine-oriented logic incorporating the equality relation Machine Intelligence Vol 4 B Meltzer and D Michie eds

Google Scholar

[11]

L Wos G A Robinson Paramodulation and set of support A Paper presented at the IRIA Symposium on Automatic Demonstration at Versailles France December 16--21 1968

Google Scholar

Cited By

View all

Manna ZWaldinger R(2005)Deduction with relation matchingFoundations of Software Technology and Theoretical Computer Science10.1007/3-540-16042-6_12(212-224)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-16042-6_12
Boyer ABoyer R(1991)A Biographical Sketch of W. W. BledsoeAutomated Reasoning10.1007/978-94-011-3488-0_1(1-29)Online publication date: 1991
https://doi.org/10.1007/978-94-011-3488-0_1
Bläsius KSiekmann J(1988)Partial unification for graph based equational reasoning9th International Conference on Automated Deduction10.1007/BFb0012846(397-414)Online publication date: 1988
https://doi.org/10.1007/BFb0012846
Show More Cited By

Completeness results for e-resolution

Recommendations

Completeness and Decidability Results for CTL in Constructive Type Theory

We prove completeness and decidability results for the temporal logic CTL in Coq/Ssreflect. Our main result is a constructive proof that for every formula one can obtain either a finite model satisfying the formula or a proof in a Hilbert system ...
On the completeness of SLDNF-resolution
Inductive Completeness of Logics of Programs

We propose a new approach to delineating logics of programs, based directly on inductive definition of program semantics. The ingredients are elementary and well-known, but their fusion yields a simple yet powerful approach, surprisingly overlooked for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

AFIPS '70 (Spring): Proceedings of the May 5-7, 1970, spring joint computer conference

May 1970

739 pages

ISBN:9781450379038

DOI:10.1145/1476936

General Chair:
Harry L. Cooke
RCA Laboratories

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 May 1970

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
145
Total Downloads

Downloads (Last 12 months)46
Downloads (Last 6 weeks)9

Reflects downloads up to 23 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Manna ZWaldinger R(2005)Deduction with relation matchingFoundations of Software Technology and Theoretical Computer Science10.1007/3-540-16042-6_12(212-224)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-16042-6_12
Boyer ABoyer R(1991)A Biographical Sketch of W. W. BledsoeAutomated Reasoning10.1007/978-94-011-3488-0_1(1-29)Online publication date: 1991
https://doi.org/10.1007/978-94-011-3488-0_1
Bläsius KSiekmann J(1988)Partial unification for graph based equational reasoning9th International Conference on Automated Deduction10.1007/BFb0012846(397-414)Online publication date: 1988
https://doi.org/10.1007/BFb0012846
Degtyarev AVoronkov A(1986)Equality control methods in machine theorem provingCybernetics10.1007/BF0106996822:3(298-307)Online publication date: May-1986
https://doi.org/10.1007/BF01069968
Manna ZWaldinger R(1985)Special relations in automated deductionAutomata, Languages and Programming10.1007/BFb0015767(413-423)Online publication date: 1985
https://doi.org/10.1007/BFb0015767
Blasius K(1983)Equality reasoning in clause graphsProceedings of the Eighth international joint conference on Artificial intelligence - Volume 210.5555/1623516.1623593(936-939)Online publication date: 8-Aug-1983
https://dl.acm.org/doi/10.5555/1623516.1623593
Bledsoe W(1983)Splitting and Reduction Heuristics in Automatic Theorem ProvingAutomation of Reasoning10.1007/978-3-642-81955-1_30(508-530)Online publication date: 1983
https://doi.org/10.1007/978-3-642-81955-1_30
Townley J(1980)A pragmatic approach to resolution-based theorem provingInternational Journal of Computer & Information Sciences10.1007/BF009822919:2(93-116)Online publication date: Apr-1980
https://doi.org/10.1007/BF00982291
PIROTTE A(1974)Automatic Theorem Proving Based on ResolutionComputer Science and Technology and their Application10.1016/B978-0-08-017806-6.50009-2(201-266)Online publication date: 1974
https://doi.org/10.1016/B978-0-08-017806-6.50009-2
Kapitonova YKostyrko VLyaletskii ADegtyarev AMalashonok AAnufriev FAsel'derov Z(1974)A brief review and bibliography of investigations into automation of search of theorem proofs in formal theoriesCybernetics10.1007/BF010684448:5(714-729)Online publication date: 1974
https://doi.org/10.1007/BF01068444
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

Completeness and Decidability Results for CTL in Constructive Type Theory

On the completeness of SLDNF-resolution

Inductive Completeness of Logics of Programs