2 papers
cs.LO2000
Boolean Satisfiability with Transitivity Constraints
Randal E. Bryant, Miroslav N. Velev
We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula Fsat encode a symmetric, transitive, binary relatio…
cs.LO1999
Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic
Randal E. Bryant, Steven German, Miroslav N. Velev
The logic of equality with uninterpreted functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic…