Publication Details
Title: A Tower Architecture for Meta-Level Inference Systems Based on Omega-OrderedHorn Theories
Author: P. E. Bonzon
Group: ICSI Technical Reports
Date: January 1995
PDF: http://www.icsi.berkeley.edu/pubs/techreports/tr-95-002.pdf
Overview:
We present a simple meta-level inference system based on a non-ground representation of both base and meta-knowledge given under the form of omega-ordered Horn theories. Processing is done via an extension of the traditional "vanilla" interpreter for logic programs, whose novel lifting mechanism allows one to hop up and down the hierarchy of theories. The resulting computational system resembles very much the tower architecture defined for functional programming. While lifting does prevent infinite recursion, successful termination depends on the actual ordering of theories. At the end, this situation amounts to facing yet another, meta-meta-level search problem. The expressive power of this system is illustrated with the solutions to various problems from the current literature, including the 3 wise men problem. It looks like a reasonable assumption to hypothesize that most (if not all) specialized reasoning performed under the label of "proofs in context" can be formulated within this system.
Bibliographic Information:
ICSI Technical Report TR-95-002
Bibliographic Reference:
P. E. Bonzon. A Tower Architecture for Meta-Level Inference Systems Based on Omega-OrderedHorn Theories. ICSI Technical Report TR-95-002, January 1995
Author: P. E. Bonzon
Group: ICSI Technical Reports
Date: January 1995
PDF: http://www.icsi.berkeley.edu/pubs/techreports/tr-95-002.pdf
Overview:
We present a simple meta-level inference system based on a non-ground representation of both base and meta-knowledge given under the form of omega-ordered Horn theories. Processing is done via an extension of the traditional "vanilla" interpreter for logic programs, whose novel lifting mechanism allows one to hop up and down the hierarchy of theories. The resulting computational system resembles very much the tower architecture defined for functional programming. While lifting does prevent infinite recursion, successful termination depends on the actual ordering of theories. At the end, this situation amounts to facing yet another, meta-meta-level search problem. The expressive power of this system is illustrated with the solutions to various problems from the current literature, including the 3 wise men problem. It looks like a reasonable assumption to hypothesize that most (if not all) specialized reasoning performed under the label of "proofs in context" can be formulated within this system.
Bibliographic Information:
ICSI Technical Report TR-95-002
Bibliographic Reference:
P. E. Bonzon. A Tower Architecture for Meta-Level Inference Systems Based on Omega-OrderedHorn Theories. ICSI Technical Report TR-95-002, January 1995