连续体假设独立性的正式证明
本文评述了最近一篇将特定形式的机器学习与集合论相关联的论文，指出集合论机制的某些部分与 Kuratowski 关于集合的有限幂的分解结果有关，并且表明在单位区间上不存在 Borel 可测单调压缩函数。
Jan, 2019
研究了 Pearl 的因果层次结构 (PCH) 框架中的推理和计算复杂性，重点关注概率和因果语言中表达的满足性问题，特别是与边缘化相关的方程，证明了不同层次和操作符的确切计算复杂性结果，以及对受限模型进行了考虑。
May, 2024
本文介绍了 CIFF 证明过程，证明了它的正确性，它是 IF 证明过程的扩展，用于处理带有数量约束的突发逻辑编程问题，同时介绍了 CIFF 系统，与最先进的突发系统和答案集求解器进行比较，并展示了如何使用它来编程一些应用程序。
Jun, 2009
提出一种新的方法来正式描述统计推断的要求并检查程序是否正确使用了统计方法。具体来说，定义了信仰 Hoare 逻辑（BHL）以形式化并推理通过假设检验获取的统计信念。证明了 BHL 对于应用在假设检验方面的问题很有用，对于合理的统计推断解释中重要的先验信念进行了澄清。
Aug, 2022
本研究介绍了反证完成的超位置演算法，用于意图性和外延句子 $\lambda$- 自由高阶逻辑，这两种形式允许部分应用和应用变量。 这些演算法由一个术语排序参数化，无需完全单调，从而可以采用 $\lambda$- 自由高阶词典路径和 Knuth-Bendix 排序。作者们在 Zipperposition prover 中实现了这些演算法，并在 Isabelle/HOL 和 TPTP 基准测试中评估它们。 它们似乎是通向完全高效自动定理证明程序的一个重要的步骤。
May, 2020
本文通过在 terms 上创建一个 measure space，定义级别逐步逼近的连续 lambda-Calculus 的典型操作语义，并定义采样基异质的语义来实现 MCMC 的 Tracing，并证明了分布语义与集成所有 Traces 的分布具有等价性，这是第一个针对高阶函数语言 Trace MCMC 的验证正确性的证明。
Dec, 2015
开发了交互式定理证明器 Isabelle，以 Horn clause 表示每个推理规则，使用基于类型的 λ 演算表示逻辑语法，支持多个逻辑系统并具有逻辑编程潜能。
Oct, 2000
介绍了 DHOL 的依赖类型扩展是如何保留了 HOL 的风格和概念框架，并且使用 DHOL 定理证明器实现了从 DHOL 到 HOL 的翻译，进而获得 DHOL 的定理证明器。
May, 2023