Probabilistic Tabled Logic Programming

Tabled resolution uses memoization to address the major shortcomings of Prolog-style resolution, namely, weak termination, repeated subcomputations, and weak semantics for negation. Several complex problems requiring fixed-point computation, including several model checking and program analysis problems, have been cast as query evaluation over logic programs and solved efficiently using tabled resolution. This project aims to combine deduction, especially tabled resolution, with probabilistic inference in order to facilitate declarative modeling and reasoning of systems with probabilistic behavior. The project includes (a) fundamental research on the semantics of probabilistic tabled resolution, (b) implementation of the research results in a robust prototype, and (c) development of applications that combine logical and probabilistic reasoniong such as probabilistic model checking of finite-state and pushdown models and probabilistic program analysis. The project addresses several problems at the level of semantics, including the treatment of programs with a mixture of continuous and discrete random variables, programs that encode dynamic models over unbounded but discrete time, and the integration of scalable probabilistic inference techniques (e.g. sampling) with deduction. At the implementation level, the project develops light-weight methods for incorporating probabilistic inference and parameter learning into a declarative programming framework called Probabilistic Tabled Logic Programming (PTLP). This framework provides a firm semantic and computational basis for combining logical and probabilistic reasoning. A computing infrastructure that tightly integrates computational logic, statistics, and constraint processing will have an immediate impact on the areas of system development and verification, planning, logistics, and optimization and control, with broad application in science and engineering.