DOI: 10.1016/0743-1066(91)80001-T
关键词:
摘要: Abstract There are numerous papers concerned with the compile-time derivation of certain run-time properties logic programs, e.g. mode inferencing, type checking, synthesis, and relevant for -parallel execution. Most approaches have little in common, they developed an ad hoc way, their correctness is not always obvious. We develop a general framework which suited to complex applications prove correctness. All states possible at run time can be represented by infinite set proof trees ( trees, SLD derivations). The core idea our approach represent this finite abstract and-or graph. present generic interpretation procedure construction such graph formulate conditions allow us construct correct one time.