逻辑程序求解的盒子模型之观察语义（扩展版）

本报告规定了一种观察语义，并对 Byrd 的盒子模型给出了原创性的表述。该方法解释了 Prolog 跟踪器的语义，而独立于任何特定实现。通常认为跟踪是相当晦涩且难以使用的。所提出的跟踪形式化表述构成了一种简单且具教学性的方法，可用于 Prolog 教学或 Prolog 跟踪器的实现。它构成了跟踪器的一种声明式规约。我们的方法突出了盒子模型使其获得成功的优点，但也指出了其缺陷与局限。事实上，所呈现的语义仅是一个示例，用于说明与跟踪器和观察过程相关的一般问题。观察过程从被观察过程中仅能获知其跟踪。因此，问题在于能否仅通过对跟踪的分析，来重构被观察过程的主要部分，并且尽可能不丢失任何信息。