GELERNTER, H Reahzatton of a geometry theorem proving machine In Computers and Thought, E Felgenbaum and J Feldman, Eds, McGraw-Hill, New York, 1963, pp 134-152

Crossref

Google Scholar

[6]

HENSCHEN, L, AND WOS, L Umt refutations and Horn sets J ACM 21, 4 (Oct 1974), 590--605

Crossref

Google Scholar

[7]

MORRIS, J B, E-resolution Extension of resolution to include the equality relation Proc First lnt Joint Conf on Artlf. lntell., 1969, pp 287-294

Google Scholar

[8]

ROBINSON, J A. A machine-oriented logic based on the resolution prmctple.L ACM 12, I (Jan. 1965), 23--41.

Crossref

Google Scholar

[9]

ROBINSON, G, AND WOS, L Paramodulatton and theorem-prowng In first-order theories wlth equahty In Machine Intelhgence 4, B Meltzer and D Mtchle, Eds, American Elsevier, New York, 1969, pp 135-150

Google Scholar

[10]

ROBINSON, G, AND WOS, L Axiom systems In automatic theorem proving Proc Syrup Automatic Demonstration, Versailles, France, 1968, M Landet, Ed, Spnnger-Verlag (Lecture Notes in Mathematics, No 125), 1970, pp 215-236

Google Scholar

[11]

RUBIN, N A hierarchical technique for mechanical theorem proving and ItS application to programming language design Courant Comptr Scl Rep No 10, New York U, New York, 1976.

Google Scholar

[12]

SHOSTAK. R E Refutation graphs Artif. Intell 7, 1 (Spnng 1976), 51-64

Google Scholar

Cited By

View all

Xu YLiu JChen SZhong XHe X(2018)Contradiction separation based dynamic multi-clause synergized automated deductionInformation Sciences10.1016/j.ins.2018.04.086462(93-113)Online publication date: Sep-2018
https://doi.org/10.1016/j.ins.2018.04.086
Lim Y(2005)The heuristics and experimental results of a new hyperparamodulation: HL-resolution8th International Conference on Automated Deduction10.1007/3-540-16780-3_94(240-253)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-16780-3_94
Schmolze J(1991)Guaranteeing serializable results in synchronous parallel production systemsJournal of Parallel and Distributed Computing10.1016/0743-7315(91)90096-R13:4(348-365)Online publication date: Dec-1991
https://doi.org/10.1016/0743-7315(91)90096-R
Show More Cited By

Index Terms

Another Generalization of Resolution
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
  2. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Logic
  2. Models of computation
    1. Computability

Recommendations

Image super-resolution: use of self-learning and gabor prior
ACCV'12: Proceedings of the 11th Asian conference on Computer Vision - Volume Part III

Recent approaches on single image super-resolution (SR) have attempted to exploit self-similarity to avoid the use of multiple images. In this paper, we propose an SR method based on self-learning and Gabor prior. Given a low resolution (LR) test image ...
VarSR: Variational Super-Resolution Network for Very Low Resolution Images
Computer Vision – ECCV 2020
Abstract
As is well known, single image super-resolution (SR) is an ill-posed problem where multiple high resolution (HR) images can be matched to one low resolution (LR) image due to the difference in their representation capabilities. Such many-to-one ...
Hyperspectral image super-resolution through clustering-based sparse representation
Abstract
Promoting the spatial resolution of hyperspectral sensors is expected to improve computer vision tasks. However, due to the physical limitations of imaging sensors, the hyperspectral image is often of low spatial resolution. In this paper, we ...

Comments

Information & Contributors

Information

Published In

Journal of the ACM Volume 25, Issue 3

July 1978

175 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/322077

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 1978

Published in JACM Volume 25, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
332
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)5

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Xu YLiu JChen SZhong XHe X(2018)Contradiction separation based dynamic multi-clause synergized automated deductionInformation Sciences10.1016/j.ins.2018.04.086462(93-113)Online publication date: Sep-2018
https://doi.org/10.1016/j.ins.2018.04.086
Lim Y(2005)The heuristics and experimental results of a new hyperparamodulation: HL-resolution8th International Conference on Automated Deduction10.1007/3-540-16780-3_94(240-253)Online publication date: 31-May-2005
https://doi.org/10.1007/3-540-16780-3_94
Schmolze J(1991)Guaranteeing serializable results in synchronous parallel production systemsJournal of Parallel and Distributed Computing10.1016/0743-7315(91)90096-R13:4(348-365)Online publication date: Dec-1991
https://doi.org/10.1016/0743-7315(91)90096-R
Sarkar DDe Sarkar S(1989)A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over IntegersIEEE Transactions on Software Engineering10.1109/32.4133015:11(1368-1381)Online publication date: 1-Nov-1989
https://dl.acm.org/doi/10.1109/32.41330
Bledsoe WHodges R(1988)A Survey of Automated Deduction11This is an enlarged version of a survey talk given by Woody Bledsoe at the Sixth National Conference on Artificial Intelligence, Seattle, Washington, July 16, 1987.Exploring Artificial Intelligence10.1016/B978-0-934613-67-5.50017-4(483-543)Online publication date: 1988
https://doi.org/10.1016/B978-0-934613-67-5.50017-4
Yamasaki SYoshida MDoshita S(1987)A fixpoint semantics of Horn sentences based on substitution setsTheoretical Computer Science10.1016/0304-3975(87)90039-951:3(309-324)Online publication date: 1-Apr-1987
https://dl.acm.org/doi/10.1016/0304-3975%2887%2990039-9
Digricoli VHarrison M(1986)Equality-based binary resolutionJournal of the ACM10.1145/5383.538933:2(253-289)Online publication date: 1-Apr-1986
https://dl.acm.org/doi/10.1145/5383.5389
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
Ohlbach HWrightson G(1984)Solving a Problem in Relevance Logic with an Automated Theorem Prover7th International Conference on Automated Deduction10.1007/978-0-387-34768-4_29(496-508)Online publication date: 1984
https://doi.org/10.1007/978-0-387-34768-4_29
Fribourg L(1983)A superposition oriented theorem proverProceedings of the Eighth international joint conference on Artificial intelligence - Volume 210.5555/1623516.1623589(923-925)Online publication date: 8-Aug-1983
https://dl.acm.org/doi/10.5555/1623516.1623589
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.

References

Cited By

Index Terms

Recommendations

Image super-resolution: use of self-learning and gabor prior

VarSR: Variational Super-Resolution Network for Very Low Resolution Images

Hyperspectral image super-resolution through clustering-based sparse representation

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations