一句话：利用动态方法在相干/几何逻辑中以证明树的有限分支消解理想对象，证明非确定性相继式的语义保守性。
抽象代数中常借助佐恩引理等引入理想对象，以证明带有有限但未必单一后继的非确定性相继式的语义保守性。动态方法被设计用来消除这类理想对象，其可行性部分源于相关领域以（有限）相干逻辑或几何逻辑为主：非确定性公理的运用可由证明树的有限分支来刻画。本文围绕有限不确定性，说明如何在这种证明论框架下动态消解理想对象，从而为语义保守性提供构造性处理。摘要未报告具体实现或实验评估。
Dynamical methods were designed to eliminate the ideal objects abstract algebra abounds with. Typically granted by an incarnation of Zorn's Lemma, those ideal objects often serve for proving the semantic conservation of additional non-deterministic sequents, that is, with finite but not necessarily singleton succedents. Eliminating ideal objects dynamically was possible also because (finitary) coherent or geometric logic predominates in that area: the use of a non-deterministic axiom can be captured by a finite branching of the proof tree.
DOI 原文 ·
@inproceedings{paperbot5494,
title = {Resolving finite indeterminacy},
author = {Peter Schuster and Daniel Wessel},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394777}
}