登入選單
返回Google圖書搜尋
註釋Abstract: "This paper gives a solution to two problems that arise in recent implementations of theorem provers for circumscription. The first problem is that, when a query contains variables, they only produce yes/no answers, rather than returning the actual values of the variables for which the query holds. The problem can be attributed to these theorem provers finding all explanations for a goal, rather than finding a minimal disjunct of these explanations. As well as providing answer extraction, we show how this technique of finding only minimal disjuncts of explanations can save much redundant computation."