paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Focusing in Orthologic

正交逻辑中的聚焦
LMCS vol.Volume 13, Issue 32017匹配度 1/10 · 该文属于纯证明论/逻辑领域，研究正交逻辑（极小量子逻辑）的切消序演算与线性逻辑聚焦技术，与用户关注的方向（静态分析、LLM/Agent 程序分析、浮点程序分析、贝叶斯程序分析）没有实质交集；虽然涉及自动证明搜索优化且附有 Coq/OCaml 实现，但缺少与 LLM、静态分析或工业落地的关联。引用 4 inbox
Olivier Laurent
定理证明与证明工程
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：为正交逻辑提出满足切消的新序演算系统，并引入线性逻辑的聚焦以优化自动证明搜索。

正交逻辑（又称最小量子逻辑）的证明搜索缺乏高效且满足切消的序演算系统。本文提出两个新的序演算：第一个基于否定词的对合性质，构造简洁的演算；第二个引入线性逻辑中的聚焦（focusing）机制，对证明施加约束以缩小搜索空间。两个系统均满足切消性质。作者进一步说明如何利用这些系统改进正交逻辑的自动证明搜索，并展示聚焦带来的效果。

问题
正交逻辑（最小量子逻辑）的证明搜索需要具有切消性质且能有效约束搜索的序演算系统。
方法
提出两个新序演算：一个依赖否定的对合性，另一个结合线性逻辑中的聚焦技术来约束证明并优化证明搜索。
评估
在正交逻辑的自动证明搜索中展示新系统（尤其聚焦系统）的优势。
原文摘要（Abstract）

We propose new sequent calculus systems for orthologic (also known as minimal quantum logic) which satisfy the cut elimination property. The first one is a simple system relying on the involutive status of negation. The second one incorporates the notion of focusing (coming from linear logic) to add constraints on proofs and to optimise proof search. We demonstrate how to take benefits from the new systems in automatic proof search for orthologic.Comment: Small rewritings. Updated benchmark section. Updated coq and ocaml files

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{Laurent17,
  title = {Focusing in Orthologic},
  author = {Olivier Laurent},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 3},
  year = {2017},
  doi = {10.23638/lmcs-13(3:6)2017}
}