Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs

DOI10.1016/J.ARTINT.2023.104045MaRDI QIDQ6152664zbMATH OpenOpenAlexFDO

Authors

Publication date 13 February 2024

Published in Artificial Intelligence (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2208.07074

zbMATH Keywords

epistemic logicknowledge representationprogram logicKripke modelstatistical hypothesis testing

Mathematics Subject Classification ID

Foundations and philosophical topics in statistics (62A01) Logics of knowledge and belief (including belief change) (03B42) Logic in artificial intelligence (68T27) Logic in computer science (03B70)

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) for formalizing and reasoning about the statistical beliefs acquired via hypothesis testing. This program logic is sound and relatively complete with respect to a Kripke model for hypothesis tests. We demonstrate by examples that BHL is useful for reasoning about practical issues in hypothesis testing. In our framework, we clarify the importance of prior beliefs in acquiring statistical beliefs through hypothesis testing, and discuss the whole picture of the justification of statistical inference inside and outside the program logic.

Recommendations

• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
• Statistical Epistemic Logic
• scientific article; zbMATH DE number 1500556
• Reasoning About States of Probabilistic Sequential Programs
• VPHL: a verified partial-correctness logic for probabilistic programs

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 2046116 (Why is no real title available?)
• scientific article; zbMATH DE number 1487488 (Why is no real title available?)
• scientific article; zbMATH DE number 755666 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 6606384 (Why is no real title available?)
• A first course in fuzzy logic
• A logic for default reasoning
• An axiomatic basis for computer programming
• An essay in modal logic
• Architecture-guided test resource allocation via logic
• Deductive software verification: from pen-and-paper proofs to industrial tools
• Dynamic Epistemic Logic and Knowledge Puzzles
• Fifty years of Hoare's logic
• From knowledge-based programs to graded belief-based programs. I: On-line reasoning
• Fuzzy sets
• GOLOG: A logic programming language for dynamic domains
• IX. On the problem of the most efficient tests of statistical hypotheses
• Knowledge-based programs
• Logical foundations of cyber-physical systems
• Programming with Infinitesimals: A While-Language for Hybrid System Modeling
• Reasoning about noisy sensors and effectors in the situation calculus
• Soundness and Completeness of an Axiom System for Program Verification
• The ASA Statement on p-Values: Context, Process, and Purpose
• The Undecidability of Monadic Modal Quantification Theory
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC

Cited in

(1)

• Statistical Epistemic Logic

This page was built for publication: Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6152664)