×

Linear resolution with selection function. (English) Zbl 0234.68037


MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Anderson, R.; Bledsoe, W. W., A linear format for resolution with merging and a new technique for establishing completeness, J. ACM, 17, 525-534 (July 1970)
[2] Andrews, P. B., Resolution with merging, J. ACM, 15, 367-381 (1968) · Zbl 0182.02506
[3] Hart, P. E.; Nilsson, N. J.; Raphael, R., A formal basis for the heuristic determination of minimum cost paths, I.E.E.E. Transactions on System Sciences and Cybernetics (July 1968)
[4] Hayes, P. J.; Kowalski, R. A., Semantic trees in automatic theorem proving, (Machine Intelligence, 4 (1969), Edinburgh University Press), 87-101 · Zbl 0217.54001
[5] Hayes, P. J.; Kowalski, R. A., Lecture notes on automatic theorem-proving, (Metamathematics Unit Memo, 40 (March 1971), University of Edinburgh)
[6] Kieburtz, R.; Luckham, D., Compatibility of Refinements of the Resolution Principle (1969)
[7] Kowalski, R. A., Search strategies for theorem-proving, (Machine Intelligence, 5 (1970), Edinburgh University Press), 181-201 · Zbl 0218.68018
[8] Kowalski, R. A., Studies in the completeness and efficiency of theorem-proving by resolution, (Ph.D. Thesis (1970), University of Edinburgh)
[9] Kuehner, D. G., A note on the relation between resolution and Maslov’s inverse method, (Machine Intelligence, 6 (1971), Edinburgh University Press), 73-76 · Zbl 0263.68049
[10] Kuehner, D. G., Strategies for improving the efficiency of automatic theorem-proving, (Ph.D. Thesis (1971), University of Edinburgh) · Zbl 0263.68049
[11] Kowalski, R. A.; Kuehner, D. G., Linear resolution with selection function, (Metamathematics Unit Memo 34 (October 1970), University of Edinburgh) · Zbl 0234.68037
[12] Loveland, D. W., A simplified format for the model-elimination theorem-proving procedure, J. ACM, 16, 349-363 (July 1969)
[13] Loveland, D. W., A linear format for resolution, (Symposium on Automatic Demonstration, Lecture Notes in Mathematics, 125 (1970), Springer-Verlag: Springer-Verlag Berlin and New York), 147-163 · Zbl 0202.01501
[14] Loveland, D. W., Some linear Herbrand proof procedures: an analysis (December 1970), Department of Computer Science, Carnegie-Mellon University
[15] Luckham, D., Refinement theorems in resolution theory, (Symposium on Automatic Demonstration, Lecture Notes in Mathematics, 125 (1970), Springer-Verlag: Springer-Verlag Berlin and New York), 163-191 · Zbl 0216.24101
[16] Maslov, S. J., Proof-search strategies for methods of the resolution type, (Machine Intelligence, 4 (1971), Edinburgh University Press), 77-90 · Zbl 0281.68042
[17] Meltzer, B., Prolegomena to a theory of efficiency of proof procedures, (Proceedings of the NATO Advanced Study Institute on Artificial Intelligence and Heuristic Programming (1971), Edinburgh University Press), 15-33
[18] Prawitz, D., Advances and problems in mechanical proof procedures, (Machine Intelligence, 4 (1969), Edinburgh University Press), 59-71 · Zbl 0257.68082
[19] Reiter, R., Two results on ordering for resolution with merging and linear format (July 1970), Department of Computer Science, University of British Columbia
[20] Robinson, J. A., A review of automatic theorem-proving, (Proceedings of Symposia in Applied Mathematics, 19 (1967)), 1-18 · Zbl 0174.29202
[21] Wos, L. T.; Carson, D. F.; Robinson, G. A., Efficiency and completeness of the set of support strategy in theorem-proving, J. ACM, 12, 687-697 (1965) · Zbl 0135.18401
[22] Yates, R. A.; Raphael, B.; Hart, J. P., Resolution Graphs, Artificial Intelligence, 1, 257-289 (1970) · Zbl 0207.02204
[23] Zamov, N. K.; Sharanov, V. I., On a class of strategies which can be used to established decidability by the resolution principle, (Issled, po konstruktivnoye matematikye i matematicheskoie logikye, III (1969), National Lending Library, Russian Translating Program 5857: National Lending Library, Russian Translating Program 5857 Boston Spa, Yorkshire), 54-64, 16
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.