Nondeterminism and Language Design in Deep Inference: A Proof Theoretic Approach to Logic Programming
Nondeterminism and Language Design in Deep Inference: A Proof Theoretic Approach to Logic Programming
复制标题
深度推理中的非确定性和语言设计：逻辑编程的证明理论方法
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Ozan Kahramanoğulları
中科院分区：
文献类型：
--
作者：
Ozan Kahramanoğulları
在深度推理中，与传统的证明论方法不同，推理规则可以在逻辑表达式中的任何深度应用。这使得设计演绎系统成为可能，这些演绎系统是为计算机科学应用程序量身定做的，否则就可能无法表达。通过深度推理，我们可以模拟传统演绎形式中的分析证明，也可以构造出更短的分析证明。然而，推理规则的深度适用性导致了证明构造中更大的不确定性。本文研究了在证明搜索中如何处理不确定性，同时保留较短的证明。通过对演绎系统的重新设计，避免了一些多余的规则应用。通过引入一种减少不确定性的新技术，可以更快地获得更短的证明，而不会破坏证明的理论性质，如割消去法。提供的不同实现允许执行实验并观察性能改进。在计算即证明搜索的观点下，我们使用这些演绎系统来开发用于规划和并发的公共证明理论语言。
In deep inference, in contrast to traditional proof-theoretic methodologies, inference rules can be applied at any depth inside logical expressions. This makes it possible to design deductive systems that are tailored for computer science applications and otherwise provably not expressible. With deep inference, we can simulate analytic proofs in traditional deductive formalisms, and also construct much shorter analytic proofs. However, deep applicability of inference rules causes a greater nondeterminism in proof construction. This thesis studies the problem of dealing with nondeterminism in proof search while preserving the shorter proofs. By redesigning the deductive systems, some redundant rule applications are prevented. By introducing a new technique which reduces nondeterminism, it becomes possible to obtain a more immediate access to shorter proofs without breaking proof theoretic properties such as cut-elimination. Different implementations presented allow to perform experiments and observe the performance improvements. Within a computation-as-proof-search perspective, we use these deductive systems to develop a common proof-theoretic language for planning and concurrency.