Π-representation: A clause representation for parallel search

作者: Daniel H. Fishman , Jack Minker

DOI: 10.1016/0004-3702(75)90005-3

关键词:

摘要: Abstract An extension to the clause form of first-order predicate calculus is described which facilitates parallel search operations. This notation, called representation (Π-representation), permits sets clauses as single “Π-clauses”. Extensions operations unification, factoring, and resolution apply this notation are also described, advantages Π-representation with respect searching, memory utilization, use semantics discussed.

参考文章(13)
Richard Char-Tung Lee, Chin-Liang Chang, Symbolic Logic and Mechanical Theorem Proving ,(1973)
Richard J Waldinger, Johns F Rulifson, Jan A Derksen, QA4: A Procedural Calculus for Intuitive Reasoning. ,(1972)
Jack Minker, James R. McSkimin, Daniel H. Fishman, MRPPS?An interactive refutation proof procedure system for question-answering International Journal of Computer & Information Sciences. ,vol. 3, pp. 105- 122 ,(1974) , 10.1007/BF00976637
Jack Minker, Daniel H. Fishman, James R. McSkimin, The Q∗ algorithm—a search strategy for a deductive question-answering system☆ Artificial Intelligence. ,vol. 4, pp. 225- 243 ,(1973) , 10.1016/0004-3702(73)90013-1
Richard E. Fikes, REF-ARF: a system for solving problems stated as procedures Artificial Intelligence. ,vol. 1, pp. 27- 120 ,(1970) , 10.1016/0004-3702(70)90003-2
W.W Bledsoe, R.S Boyer, W.H Henneman, Computer proofs of limit theorems Artificial Intelligence. ,vol. 3, pp. 27- 60 ,(1972) , 10.1016/0004-3702(72)90041-0
David Luckham, Nils J. Nilsson, Extracting information from resolution proof trees Artificial Intelligence. ,vol. 2, pp. 27- 54 ,(1971) , 10.1016/0004-3702(71)90003-8
J. A. Feldman, J. R. Low, D. C. Swinehart, R. H. Taylor, Recent developments in SAIL Proceedings of the December 5-7, 1972, fall joint computer conference, part II on - AFIPS '72 (Fall, part II). pp. 1193- 1202 ,(1972) , 10.1145/1480083.1480158