zbMATH — the first resource for mathematics

An automated theorem prover for the probability logic LPP. (English) Zbl 1274.03041
Krapež, A. (ed.), A tribute to S. B. Prešić. Papers celebrating his 65th birthday. Beograd: Matematički Institut SANU. 79-83 (2001).
Summary: We consider a propositional probability logic denoted LPP. LPP is a conservative extension of classical propositional logic. The language of LPP contains probability operators of the form \(P_{\geq s}\) for every real number \(s\in[0,1]\). The intended meaning of a formula of the form \(P_{\geq s}\alpha\) is ‘\(\alpha\) holds with probability at least \(s\)’. We obtain a decision procedure for LPP by reducing probability formulas to systems of linear equalities and inequalities. We describe an automated theorem prover based on this procedure.
For the entire collection see [Zbl 0977.00051].
03B48 Probability and inductive logic
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)