登入選單
返回Google圖書搜尋
Procedural Interpretation of Non-Horn Logic Programs
註釋Abstract: "Procedural interpretation in logic programming consists of two parts: answering positive queries and answering negative queries. Answering postitive queries can be done using a general theorem prover. To answer negative queries it is necessary, in most practical cases, to augment a theorem prover with default rules. Such an approach has been taken with Horn clause logic programs in the definition of SLDNF-resolution [Cla78]. We describe a similar proof procedure for non-Horn programs and define an inference system, SLINF-resolution, for this purpose. SLI-resolution is used as the main inference mechanism and a weaker form of the generalized closed world assumption [Min82], called the Support-for Negation Rule, is used as the default rule for answering negative queries."