×

zbMATH — the first resource for mathematics

Linear resolution with selection function. (English) Zbl 0234.68037

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
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, (), 87-101 · Zbl 0217.54001
[5] Hayes, P.J.; Kowalski, R.A., Lecture notes on automatic theorem-proving, ()
[6] Kieburtz, R.; Luckham, D., Compatibility of refinements of the resolution principle, (1969)
[7] Kowalski, R.A., Search strategies for theorem-proving, (), 181-201 · Zbl 0218.68018
[8] Kowalski, R.A., Studies in the completeness and efficiency of theorem-proving by resolution, ()
[9] Kuehner, D.G., A note on the relation between resolution and Maslov’s inverse method, (), 73-76 · Zbl 0263.68049
[10] Kuehner, D.G., Strategies for improving the efficiency of automatic theorem-proving, () · Zbl 0263.68049
[11] Kowalski, R.A.; Kuehner, D.G., Linear resolution with selection function, () · 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, (), 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, (), 163-191 · Zbl 0216.24101
[16] Maslov, S.J., Proof-search strategies for methods of the resolution type, (), 77-90 · Zbl 0281.68042
[17] Meltzer, B., Prolegomena to a theory of efficiency of proof procedures, (), 15-33
[18] Prawitz, D., Advances and problems in mechanical proof procedures, (), 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, (), 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, (), 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.