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

DOI10.1016/J.ARTINT.2023.104045arXiv2208.07074OpenAlexW4388571844MaRDI QIDQ6152664FDOQ6152664

Authors:

Publication date: 13 February 2024

Published in: Artificial Intelligence (Search for Journal in Brave)

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.

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

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

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)

Cites Work

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

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)