DOMAINS :: SMT-LIB :: Update

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. Update

tinelli wrote at Apr 01, 2004 - 01:19 AM
---------------------------------------------------------------------
Dear all,

although this list has been dormant in the last few months, we have continued working on SMT-LIB in the background (and as our other committments permitted). At long last here is an update.

Index:

0. New emailing list
1. Sorts vs. no sorts
2. Other enhancements on the SMT-LIB format
3. NSF Proposal on SMT-LIB
4. The PDPAR'04 workshop


0. New emailing list

First a service announcement. We are moving this discussion list to a discussion forum within the QPQ website (Please check http://www.qpq.org/ if you are not familiar with QPQ. Also, Shankar will be happy to give you further details if you have additional questions on the QPQ project at SRI.)

To have access to the discussion you will need to create an account on QPQ, if you do not already have one, and subscribe to the SMT-LIB forum.
After that, you'll be able to receive all posted messages to the email address you specify and access them with a web browser as well.
Of course you will also be able to post messages yourself via the web interface.

I have posted on the forum all messages sent to this list so far, for archival purposes. Please note that

        ***the current list will be discontinued on April 15***

so make sure you subscribe to the QPQ forum by then if you want to continue participating to the SMT-LIB discussion.


1. Sorts vs. no sorts

As you may recall, several issues concerning SMT-LIB were discussed at a panel during PDPAR last year. One of the major points of contention was whether the SMT-LIB language should be sorted or unsorted.
At the end, the panel recommended that we investigate more and then decide ourselves.
After several off-line discussions with several of you and with other people, and a few more background readings we concluded that the advantages of having sorts (and subsorts) outstrip the disadvantages. Hence, we decided to go for a sorted framework.
The question then became what kind of order-sorted logic to adopt, as there are several conceivable, non-equivalent variants.
We have considered a few and concluded that ... further investigation is needed

More seriously, we have a pretty good idea now of what would be a good order-sorted framework for SMT-LIB but there are a few more kinks that need to be checked.
So, in the interest of moving forward with the project we have decided to produce a first version of the SMT-LIB format that is only many-sorted, that is, allows sorts but no subsorts.
The idea is to extend the format later in a second version of the language, but get started in the meantime with theories and benchmarks that do not need subsorts.
Since there is only one sensible way really to define a many-sorted language and logic, the task is simpler and unproblematic (if not as general as we need).

We are going to post a white paper on the first version of the SMT-LIB format and logic soon.


2. Other enhancements on the SMT-LIB format

We have collected a few additional suggestions from some of you on improving the format, that are orthogonal to the sorts issue. We will present those as well in the white paper.


3. NSF Proposal on SMT-LIB

As several of you already know, with Aaron Stump and Clark Barrett with have developed and submitted to the Naional Science Foundation a collaborative project proposal built around the SMT-LIB initiative. If approved, the project will help us commit more resources to the initiative and hopefully make it more successful. So keep your finger crossed.


4. The PDPAR'04 workshop

Most of you should have received a CFP for PDPAR'04, which we are organizing this year again.
We urge everbody again to consider submitting a contribution, as you represent a large part of PDPAR's target community.
The submission deadline is next week (but we will entertain any reasonable requests of extension).
More details on PDPAR'04 can be found at http://www.loria.fr/~ranise/pdpar04/


Best,


Cesare and Silvio


---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=16&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=16

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/