theorem prover in Oz

[Juergen Stuber]

Hi Fred,

fsp at info.ucl.ac.be (Fred Spiessens) writes:
> Hi Jrgen, Hi all,

thanks for the reply, and also to Andr‚ Rifaut who replied privately.

> last week, at the ICLP03/ASIAN03 conference, I got an
> Oz-related question from Jrgen Stuber (Loria), who I
> presume is not on this userlist (yet).

I'm now reading it via news, let's see if this works.

> He wanted to know about theorem provers available in Oz,
> and/or if it was easy to make them, and how Oz constraint
> programming would fit that picture.
> I don't know much about this domain, but I promised him a
> few references, and this is what I found until now:
>
> http://www.ps.uni-sb.de/~niehren/ozded.html

I looked through that, but it seems that most theorem provers
are of the tableaux/model elimination variety, where you explore
a space of possible models.  I can see that Oz is well-suited to that,
but I'm more interested in resolution/paramodulation style theorem proving, 
where the only thing I saw is the resolution prover for propositional
logic in Exercise 16.

Andr‚ mentioned http://www.activemath.org/ and
http://www.ags.uni-sb.de/~omega/, where Oz seems to be used
for proof planning and communication.
He also mentioned an implementation of Positive Unit Hyper Resolution (PUHR)
by Karsten Konrad (http://citeseer.nj.nec.com/92952.html)
that seems however to have disappeared from the face of the web.
I think this wouldn't tell us too much about general resolution,
because the unit clauses make it especially simple to use some form
of propagation.

So I guess for a resolution style prover one would not have too much
support from the language, and be happy when it doesn't make the job
more difficult than necessary.


That said, the real question that I posed to Fred was how easy it would
be to do Constraint Handling Rules (CHR) style of constraint solving in Oz.
There you are not interested in assigning concrete values to variables,
instead you have multisets (conjunctions) of atoms and you want to know
mostly whether they are satisfiable, but also whether two constraints
imply each other or are equivalent.  The semantics of your constraints
are defined by rewrite rules on these multisets, that may add atoms
(propagate), replace or delete them (simplify) or combinations thereof.
Typical examples I would be interested in are congruences and orderings
on terms (so in particular these are not finite domain constraints).

Would Oz' features make it easy to implement that efficiently?

How about Alice?

How do they perform on large datastructures (sets of clauses)?


Jrgen

-- 
Jrgen Stuber <stuber at loria.fr>
http://www.loria.fr/~stuber/
-
Please send submissions to users at mozart-oz.org
and administriva mail to users-request at mozart-oz.org.
The Mozart Oz web site is at http://www.mozart-oz.org/.
Please send bug reports to bugs at mozart-oz.org.