T Walsh CIAO 2001 Presentation Abstract

I describe a new application for proof planning: generating logical consequences of a 
theory that, when added to a constraint program as implied constraints, reduce search. 
I outline a number of methods for generating useful logical consequences including 
eliminate (which performs Gaussian-like variable elimination), introduce (which introduces 
new variables for shared subterms), linearize (which tries to linearize non-linear 
constraints), all-different (which reasons about variables which take distinct values), 
and symmetry (which tries to break symmetries). I also discuss some new applications for 
old favourites from PRESS like isolate, collect, and attract.