An automated theorem prover for the probability logic LPP. (English) Zbl 1274.03041

Rašković, Miodrag; Ognjanović, Zoran; Petrović, Vladimir; Majstorović, Uroš

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)