返回Google圖書搜尋

A Mixed Top-down and Bottom-up Deduction Method and Its Correctness

Thomas J. Watson IBM Research CenterC. Beckstein

出版	IBM Thomas J. Watson Research Division, 1989
URL	http://books.google.com.hk/books?id=0-RSHwAACAAJ&hl=&source=gbs_api

註釋We show that the method is sound, that it is strongly complete (terminating) for function-free programs with negation, and complete for programs without negation if function symbols are allowed. Soundness and completeness are with respect to the stratified model theory of [2]. The method uses the call graph of an object-program to represent static dependencies, and a Truth Maintenance System to store dynamic dependencies between partial lemmas generated by the deduction method. We argue by means of examples that these dependencies allow the method to avoid some redundant deductions, and that they are useful in forward reasoning in the presence of negation-as-failure."