I Miguel Uppsala 23 May 2001: Presentation Abstract

Implied  constraints are those that logically  follow from the initial
model of a constraint  satisfaction  problem.  The addition of implied
constraints can greatly improve efficiency and is an important step in
solving  difficult  problems.  Unfortunately,  the addition of implied
constraints  is  currently  done by hand in an ad-hoc  manner.  We are
developing  a  system  based  on  proof   planning   which   generates
automatically  those  implied  constraints  which  will help to reduce
search.

Proof planning is a technique  used for guiding the search for a proof
in  automated   theorem   proving.  Common   patterns  in  proofs  are
identified and  encapsulated  in methods which are made available to a
planner.  This talk describes how proof planning is being  extended to
generate  implied  algebraic   constraints.  This  inference   problem
introduces  a  number  of   challenging   problems  like   deciding  a
termination  condition  and  evaluating  constraint  utility.  We have
implemented  a  number  of  methods  for  reasoning  about   algebraic
constraints.   For   example,   the   "eliminate"    method   performs
Gaussian-like   elimination  of  variables  and  terms.  We  are  also
re-using  proof methods from the PRESS  equation  solving  system like
(variable) isolation.