极性与聚焦：从可实现性到自动推理之旅
摘要
本论文探讨了极性和聚焦在计算逻辑各个方面中的作用。这些概念在经典逻辑语境下将证明解释为程序（即 Curry-Howard 对应）中起着关键作用。它们源于线性逻辑，允许为经典逻辑中的消切构造有意义的语义，其中一些与函数式编程中的按名调用和按值调用规则相关。本论文的第一部分介绍了这些解释，强调了极性和聚焦的作用。例如：正公式的证明提供结构化数据，而负公式的证明消耗此类数据；聚焦允许将两类证明之间的交互描述为纯模式匹配。本论文的第二部分进一步推进了这一思想，并将其与可实现性语义联系起来，其中结构化数据被代数地解释，而此类数据的消耗则通过正交关系建模。该部分的大部分内容已在 Coq 证明助手中得到证明。极性和聚焦的引入也着眼于逻辑编程的应用，其中计算即证明搜索。在本论文的第三部分，我们通过探索这些概念在证明搜索的其他应用（如定理证明，特别是自动推理）中的作用，进一步推进了这一思想。我们利用这些概念描述了 SAT 求解器和 SMT 求解器的主要算法：DPLL。随后，我们描述了一个名为 Psyche 的证明搜索引擎的实现。其架构基于聚焦概念，提供了一个平台，使得来自自动推理的智能技术（或用户界面）可以通过使用 API 安全且可靠地实现。
引用
@article{arxiv.1412.6781,
title = {Polarities & Focussing: a journey from Realisability to Automated Reasoning},
author = {Stéphane Graham-Lengrand},
journal= {arXiv preprint arXiv:1412.6781},
year = {2014}
}
备注
Dissertation submitted towards the degree of Habilitation \`a Diriger des Recherches. Universit\'e Paris-Sud. 212 pages. Thesis publicly defended on 17th December 2014 before a panel consisting of Laurent Regnier, Wolfgang Ahrendt, Hugo Herbelin, Frank Pfenning, Sylvain Conchon, David Delahaye, Didier Galmiche, Christine Paulin-Mohring