Accession Number:

ADA461197

Title:

Reducing Separation Formulas to Propositional Logic

Descriptive Note:

Technical rept.

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Report Date:

2003-04-16

Pagination or Media Count:

22.0

Abstract:

We show a reduction to propositional logic from a Boolean combination of inequalities of the form Vi is greater or equal Vj C and Vi is less than Vj C where C is a constant, and Vi, Vj are variables of type real or integer. Equalities and uninterpreted functions can be expressed in this logic as well. We discuss the advantages of using this reduction as compared to competing methods, and present experimental results that support our claims.

Subject Categories:

  • Theoretical Mathematics
  • Operations Research

Distribution Statement:

APPROVED FOR PUBLIC RELEASE