Semantical Properties of SLD-Resolution with Reflection
LEON S. STERLING · 1995
We present the properties of an approach to giving a formal declarative and fixed point semantics to metalogic languages and systems including some form of encoding (naming device), and metalevel and/or multilevel computation. The starting point is the semantic framework proposed by Jaffar et al [3]. The main components of the proposed approach are the following. (i) An extended first-order language providing names for its own expressions; the syntax for names in this language is general and abstract enough to subsume many possible forms of concrete naming conventions. (ii) Rules for relating names to what is named, expressed by means of an equational theory that extends the Clark's equality theory. (iii) A corresponding rewrite system for extended unification, with certain similarities to a constraint solving system over names. (iv) A formalization of metalevel and multilevel computation by means of an extended SLD-resolution [1]. It includes a form of logical reflection that allows the level where deduction is performed to change according to predefined conditions, specific of a given system/language. The main contributions of the work are in two (related) directions. First, the extended SLD-resolution is proved to be sound and complete, provided that some requirements are fulfilled by the chosen naming policy and rewrite system for unification. Second, by discussing these requirements, the proposed semantic framework is shown to be general enough to constitute a ground work suitable for: (i) the possible integration of metaprogramming and constraint logic programming, so as to render the design of more flexible and powerful logic languages a concrete possibility; (ii) a discussion and comparison of various forms of encodings with respect to their impact on the semantic behaviour of extended resolution.