DOMAINS :: SMT-LIB :: Decision procedures for algebraic datatypes

[Silvio.Ranise@loria.fr]

Dear Sava,

there has been a paper co-authored by Manna at last IJCAR
in Cork considering (if I remember correctly) the full theory
of recursive data types. I think that paper besides being
relevant to recursive datatypes it is also interesting since
it offers some more pointers to the literatures which include
those you have cited in your mail.

Also, there is also some work we (meaning me, Pascal Fontaine, and
Calogero Zarba) have done on combining lists (a kind of recursive
data types) with a non-stably infinite theory of elements contained
in the lists and a length function over lists.  This is going to
be published at next LPAR.  Here is a preliminary bibentry for the work:

Pascal Fontaine, Silvio Ranise, and Calogero G. Zarba.
Combining lists with non-stably infinite theories.
Logic Programming and Automated Reasoning, 2005 (LPAR'05). To appear.

If you are interested in the paper, indeed, I can send a copy to you
as soon as the final version is ready.
Also in our paper, you can find some pointers to the literature and
a precise bibentry for the paper by Manna and others that I have mentioned
above.

I hope this is helpful.

Regards,

Silvio.



Selon QPQ <saadati at csl.sri.com>:

> Forums QPQ
> DOMAINS :: SMT-LIB ::.. Decision procedures for algebraic datatypes
>
> savakrstic wrote at Jan 24, 2005 - 10:24 AM
> ---------------------------------------------------------------------
> I'd like to ask this forum about references for decision procedures
> for (the quantifier free theory) of algebraic datatypes, also known as
> recursive datatypes. Early papers by Nelson & Oppen and Shostak
> contain decision procedures for lists. Nikolaj Bjoerner's thesis
> (1988) contains a general account. What else is there that we should
> know about and cite?
>
> Thanks,
>
> Sava
>
> ---------------------------------------------------------------------
>
> Reply to this message:
>
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=56&forum=46
>
> Browse thread:
>
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=56
>
> You are receiving this Email because you are subscribed to be notified of
> events in forums at: http://www.qpq.org/
>