© 1996 by Oxford University Press
Original Articles |
On the Declarative and Procedural Semantics of Definite Metalogic Programs
School of Computing and Information Technology, Griffith University Nathan, Qld 4111, Australia. E-mail: chris{at}cit.gu.edu.au
We present declarative and procedural semantics for an amalgamation of object language and metalanguage. We define the class of definite metalogic programs, based on a definite clause language, a binary demonstration predicate, and a naming scheme with both primitive and structured names. The declarative semantics is an extension of the semantics of logic programs dealing with multiple theories and names. The procedural semantics uses a resolution rule and a constructive meta-level to object-level reflection rule.
Keywords: Amalgamation; metalogic; meta-programming; reflection; demo; names