TY - RPRT
T1 - DDDLIB: A Library For Solving Quantified Difference Inequalities
AU - Møller, Jesper B.
PY - 2002/2
Y1 - 2002/2
N2 - DDDLIB is a library for manipulating expressions in a first-order logic over Boolean variables and inequalities of the form x1-x2<=d, where x1,x2 are real variables and d is an integer constant. expressions are represented in a semi-canonical data structure called difference decision diagrams (ddds) which provide efficient algorithms for constructing expressions with the standard boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties (satisfiability, validity and equivalence). the library is written in c and has interfaces for c++, moscow ml and ocaml.
AB - DDDLIB is a library for manipulating expressions in a first-order logic over Boolean variables and inequalities of the form x1-x2<=d, where x1,x2 are real variables and d is an integer constant. expressions are represented in a semi-canonical data structure called difference decision diagrams (ddds) which provide efficient algorithms for constructing expressions with the standard boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties (satisfiability, validity and equivalence). the library is written in c and has interfaces for c++, moscow ml and ocaml.
KW - first-order logic
KW - difference decision diagrams
KW - satisfiability
KW - Boolean operators
KW - quantifier elimination
M3 - Report
T3 - IT University Technical Report Series
BT - DDDLIB: A Library For Solving Quantified Difference Inequalities
PB - IT-Universitetet i København
CY - Copenhagen
ER -