用于统计假设测试程序的声音且相对完全的信念 Hoare 逻辑

Aug, 2022

用于统计假设测试程序的声音且相对完全的信念 Hoare 逻辑

Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs

Yusuke Kawamoto, Tetsuya Sato, Kohei Suenaga

TL;DR提出一种新的方法来正式描述统计推断的要求并检查程序是否正确使用了统计方法。具体来说，定义了信仰 Hoare 逻辑（BHL）以形式化并推理通过假设检验获取的统计信念。证明了 BHL 对于应用在假设检验方面的问题很有用，对于合理的统计推断解释中重要的先验信念进行了澄清。

Abstract

We propose a new approach to formally describing the requirement for statistical inference and checking whether a program uses the statistical method appropriately. Specifically, we define belief hoare logic (BHL

statistical inference belief hoare logic hypothesis testing prior beliefs program logic

发现论文，激发创造

关于信念程序的验证

本文提出了一种基于动作和信念的模态逻辑形式化描述信念程序的方法，用以表达类似 PCTL 的时态属性，并探讨验证信念程序的可判定性和不可判定性。

Apr, 2022

随机逻辑程序：采样、推理及应用

本研究介绍了基于变量消除和重要性采样的精确和近似概率推理算法，并展示了如何使用 SLPs 股票机器学习的先验分布，包括逻辑程序和贝叶斯网结构。作者还应用 Metropolis-Hasting 算法，构建了一个从后验分布中采样的马尔科夫链，同时讨论了构建后验明确表示的可能性。

Jan, 2013

稳定模型与一种替代逻辑编程范式

通过稳定模型语义重新审视逻辑编程在约束满足问题中的角色定义，提出一种函数符号被消除的新型逻辑编程系统，基于约束来描述问题的解决方案。该方法具有良好的应用范围、有力的计算算法和新型编程方法。

Sep, 1998

概率逻辑程序的语义和复杂度

本文研究基于 Sato 分布语义的概率逻辑程序，分析了基于稳定和基于良基模型这两种语义，探讨了 credal 语义产生的概率模型集合是无限单调 Choquet 容量的结果产生的几个有用的结果，并研究了其推理和查询的复杂度。作者对此进行了详细说明，并对无环、分层、周期性的命题和关系程序，提出了推理和查询复杂度的结果，该复杂度达到各种计数层次和指数级别。

Jan, 2017

三十年的认知规范

该研究论文介绍了认知逻辑程序的语言和形式语义，并探讨了该领域的当前状态和未来研究的挑战。

Aug, 2021

一个有限置信一阶逻辑推理系统

本文提出了一种高度可表达的有限置信逻辑，可以进行可计算的推理，在一阶逻辑上保持可判定性，在命题逻辑上保持可操作性，并引入一种采用此逻辑作为表示语言的推理系统，该系统展示了有限置信的好处。

May, 2017

StatWhy：统计假设检验程序的形式化验证工具

应用形式化规范方法和自动验证技术，开发了一种检验统计程序正确性的新方法，可以避免在科学研究中广泛存在的统计方法滥用和误解问题。

May, 2024

概率编程中逻辑推理的魔力

本论文提出了一种基于分布句式的逻辑推理方法，并结合前向推理和重要性抽样技术，采用魔法集和后向推理技术来实现高效的概率推理。

Jul, 2011

扩展和实现稳定模型语义

提出了一种用于计算逻辑程序稳定模型语义的算法，强调使用有效的实现技术，特别地，提出了一种展望的实现和一种通过最小化搜索空间来产生良好的启发式方法。结果表明，稳定模型语义的逻辑程序具有更紧凑的逻辑程序表示，因此在某些问题上比命题逻辑优越。

May, 2000

统一逻辑蕴涵和统计估计

本文基于生成模型的思想，采用 Bayesian learning 方法，探究形式逻辑及其数理统计特性，构建了一个统一的形式逻辑和统计推理理论。

Feb, 2022