Combining nondeterminism, probability, and termination: equational and metric reasoning

依赖类型理论中单子等式推理的实用形式化

A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory

该研究在Coq证明助手中以接口形式形式化单子效应层级与代数定律，分离定律与模型，结合Coq重写能力与引理库实现简洁程序证明，还可用于单子模型形式化及含引用ML子集的等式定律设计。

案例研究：等式理论中的饱和作为显式模型

Case Study: Saturations as Explicit Models in Equational Theories

本文提出通过饱和集构建显式模型的方法，用于等式理论中的反模型生成，并展示了其在Vampire和E中的实现及应用。

面向随机非确定性的恶魔结果逻辑

A Demonic Outcome Logic for Randomized Nondeterminism

本文提出恶魔结果逻辑，用于统一推理同时包含随机化和非确定性的程序，通过等式法则、循环规则及多个案例研究展示其能力。

Hypertableau Reasoning for Description Logics

We present a novel reasoning calculus for the description logic SHOIQ^+---a knowledge representation formalism with applications in areas such as the Semantic Web. Unnecessary nondeterminism and the construction of large models are two primary sources of inefficiency in the tableau-based reasoning calculi used in state-of-the-art reasoners. In order to reduce nondeterminism, we base our calculus on hypertableau and hyperresolution calculi, which we extend with a blocking condition to ensure termination. In order to reduce the size of the constructed models, we introduce anywhere pairwise block…

XPL: An extended probabilistic logic for probabilistic transition systems

Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of reactive probabilistic systems. We explore XPL, an extension to GPL allowing the semantics of nondeterminism present in Markov decision processes (MDPs). XPL is expressive enough that a number of independently studied problems--- such as termination of Recursive MDPs (RMDPs), PCTL* model checking of MDPs, and reachability for Branching MDPs--- can all be cast as model checking over XPL. Termination of multi-exit RMDPs is undecidable; thus, model checking in XPL is undecidable…

遗忘概率结果逻辑：使用遗忘对手验证概率程序

Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary

研究概率程序中由遗忘对手控制不确定性的推理问题，引入opOL逻辑，基于结果逻辑和概率分离逻辑建模，为随机和非确定性结果分析及证明终止性提供规则，经案例研究测试表现力并在Lean 4中实现机械化。

Verification of Nondeterministic Quantum Programs

Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and the termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian ope…

概率策略：可定义性与张量完备性问题

Probabilistic Strategies: Definability and the Tensor Completeness Problem

本文研究概率策略的可定义性与张量完备性问题，证明在概率选择或I/O操作有限时迹等价完备，并刻画良基程序语义对应胜利策略，同时将结果与计算效应单子建立联系。