Ofer Strichman: A Propositional World

(joint work with Randal Bryant and Sanjit Seshia).

Abstract: Most decidable infinite-state theories are solved with decision procedures that are designed to handle conjunctions of constraints, while disjunctions are handled by 'case splitting'. This means that even if the decision procedure is efficient, there can still be an exponential number of sub-formula to solve. When a theory can be decided through an efficient reduction to a finite-state problem (e.g., a reduction to propositional logic), the explicit case splitting is avoided. Furthermore, since many decidable theories already have known efficient representations as propositional formulas, this gives rise to the possibility of combining theories on the propositional logic level.

The talk will start by discussing the principle differences between these two approaches. It will then focus on such a reduction from a subset of linear arithmetic called eparation predicates', i.e., inequalities of the form x > y + c where c is a constant and x, y are variables of type real or integer (equalities and uninterpreted functions can be expressed in this logic as well). An extension of this theory to the full linear arithmetic will be discussed as well.

Short CV: Ofer Strichman Received his B.Sc and M.sc from the Technion in Operations Research and System Analysis, and his Ph.D in Computer Science from the Weizmann Institute (Israel). His Ph.D. thesis, under the guidance of Prof. Amir Pnueli, covered various subjects in formal verification like Translation Validation, decision procedure for Equality Logic and Bounded Model Checking. He is currently a post-doc in Prof. Ed Clarke's group.