Logic programming is a declarative programming paradigm. Programming language Prolog makes logic programming possible, at least to a substantial extent. However the Prolog debugger works solely in terms of the operational semantics. So it is incompatible with declarative programming. This report discusses this issue and tries to find how the debugger may be used from the declarative point of view. The results are rather not encouraging.
Also, the box model of Byrd, used by the debugger, is explained in terms of SLD-resolution.
Prolog is a well known declarative programming language based on propositional Horn formulas. It is useful in various areas, including artificial intelligence, automated theorem proving, mathematical logic and so on. An active research area for many years is to extend Prolog to larger classes of logic. Some important extensions of it includes the constraint logic programming, and the object oriented logic programming. However, it cannot solve problems having arbitrary quantified Horn formulas. To be precise, the facts, rules and queries in Prolog are not allowed to have arbitrary quantified va…
University of North Texas（北德克萨斯大学）；Topos Institute（Topos研究所）
The problem we want to solve is how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. We start by filtering for linearity the proof terms associated by our Prolog-based theorem prover for Implicational Intuitionistic Logic. This works, but using for each formula a PSPACE-complete algorithm limits it to very small formulas. We take a few walks back and forth over the bridge between proof terms and theorems, provided by the Curry-Howard isomorphism, and derive step-by-step an efficient algorithm requiring a low polynomial effort …
Reversible debugging is becoming increasingly popular for locating the source of errors. This technique proposes a more natural approach to debugging, where one can explore a computation from the observable misbehaviour backwards to the source of the error. In this work, we propose a reversible debugging scheme for logic programs. For this purpose, we define an appropriate instrumented semantics (a so-called Landauer embedding) that makes SLD resolution reversible. An implementation of a reversible debugger for Prolog, rever, has been developed and is publicly available.
Tabling, Rational Terms, and Coinduction Finally Together!
逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）列表是逻辑编程中常用的技术，用于避免逻辑程序的循环行为并实现更多的声明性程序定义。此外，制表通常可以提高计算性能。有理项是指具有一个或多个无穷子项但具有有限表示的项。在Prolog中，当统一两个术语时，可以通过省略发生检查来生成有理术语。有理项的应用包括确定子句文法、约束处理系统和共归纳。在本文中，我们报告我们的扩展YAP的Prolog制表机制，以支持合理的条款。我们描述了表空间中有理项的内部表示，并证明了它的正确性。然后，我们使用这个扩展来实现一个基于表格的方法coinduction。我们比较我们的方法与当前的共归纳变换，并描述了实现。此外，我们提出了一个算法，确保一个规范的表示为合理的条款。
