# 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].
##### MSC:
 03B48 Probability and inductive logic 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)