A logic with imprecise probabilities and an application to automated reasoning using rewriting techniques

A new probabilistic logic for handling imprecise probabilities is introduced, implemented in a rewriting system, and used to carry out an experiment. Each well-formed formula of the probabilistic logic is labeled with two values that represent possible minimum and maximum probabilities associated with the event related to the unlabeled formula. The aim of this logic is to facilitate application of rules to obtain an approximation of the probability interval associated with an event, without the necessity of knowing the precise probability of other events. The logic is described as a formal theory by means of its language, semantics and a proof theory. The soundness of the proof theory has been proven. Rewriting techniques are a powerful method for testing the behavior of a formal proof calculus through translation of calculus inference rules into rewrite rules. Implementation of the logic rules in a rewriting language such as Maude allows an automated reasoning system to be easily obtained, which can be consulted by applications. We developed a small game application and an experiment to test the application.