A Tower Architecture for Meta-Level Inference Systems Based on Omega-OrderedHorn Theories

TitleA Tower Architecture for Meta-Level Inference Systems Based on Omega-OrderedHorn Theories
Publication TypeTechnical Report
Year of Publication1995
AuthorsBonzon, P. E.
Other Numbers942
Abstract

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.

URLhttp://www.icsi.berkeley.edu/pubs/techreports/tr-95-002.pdf
Bibliographic Notes

ICSI Technical Report TR-95-002

Abbreviated Authors

P. E. Bonzon

ICSI Publication Type

Technical Report