Request for references

From: Ulrich Scholz (d4_at_thispla.net)
Date: 11/30/03 

Date: Sun, 30 Nov 2003 14:17:04 +0100

Dear all,

I've done some work with constraint programming and theorem proving.
I'm sure that I'm not the first who tried the following approach - a
theorem prover as subsystem of a system which is implemented by
constraint programming. If you know of related work, please tell me.

Thank you, Uli

I've implemented a planning technique to find replaceable action
sequences. While similar techniques usually uses a ground
representation of actions and sequences, my implementation
uses a generalized representation by combining constraint programming
and theorem proving.

The program uses constraint programming to construct candidate sequence
for the replacement of a target sequence. The resulting constraints are
used to construct a first order formula that is valid if and only if
every ground instance of the target sequence is replaceable by an ground
instance of a candidate. The formula is then given to a theorem prover,
which decides whether or not the target sequence is replaceable.

Of course, I know of one example in planning where a theorem prover is
used as subsystem: The STRIPS planner uses QA3 to establish the truth of
  action preconditions. 

-- 
Ulrich Scholz
d @ h s l . e
  4 t i p a n t --- http://thispla.net