From owner-mizar-forum-outgoing@mizar.uwb.edu.pl Thu Apr 7 19:53:49 2005 Return-Path: X-Original-To: mizar-forum-outgoing Delivered-To: mizar-forum-outgoing@mizar.uwb.edu.pl Received: by mizar.uwb.edu.pl (Postfix, from userid 28) id 5693215329; Thu, 7 Apr 2005 19:53:45 +0200 (CEST) X-Original-To: mizar-forum@mizar.uwb.edu.pl Delivered-To: mizar-forum@mizar.uwb.edu.pl Received: from mailgate.uwb.edu.pl (mailgate.uwb.edu.pl [212.33.71.77]) by mizar.uwb.edu.pl (Postfix) with ESMTP id 2981014FBE for ; Thu, 7 Apr 2005 19:53:45 +0200 (CEST) Received: from smtp1.ms.mff.cuni.cz (ns.ms.mff.cuni.cz [195.113.20.71]) by mailgate.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j37HrcfP014124 for ; Thu, 7 Apr 2005 19:53:39 +0200 Received: from ktilinux.ms.mff.cuni.cz (ktilinux.ms.mff.cuni.cz [195.113.17.207]) by smtp1.ms.mff.cuni.cz (8.13.3/8.13.3) with ESMTP id j37HrVGO051362 for ; Thu, 7 Apr 2005 19:53:32 +0200 (CEST) Received: from localhost (urban@localhost) by ktilinux.ms.mff.cuni.cz (8.11.6/linuxconf) with ESMTP id j37GrtI10238 for ; Thu, 7 Apr 2005 18:53:55 +0200 Date: Thu, 7 Apr 2005 18:53:55 +0200 (CEST) From: Josef Urban To: Subject: Re: [mizar] Mizar ver. 7.3.01 released In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Received-SPF: none (mailgate.uwb.edu.pl: urban@ktilinux.ms.mff.cuni.cz does not designate permitted sender hosts) receiver=mailgate.uwb.edu.pl; client-ip=195.113.20.71; helo=smtp1.ms.mff.cuni.cz; envelope-from=urban@ktilinux.ms.mff.cuni.cz; x-software=spfmilter 0.95 http://www.acme.com/software/spfmilter/ with libspf2; X-UwB_mailgate-MS-Information: Uniwersytet w Bialymstoku; e-mail: dask(at)uwb.edu.pl X-UwB_mailgate-MS: Found to be clean X-UwB_mailgate-MS-SpamCheck: not spam X-UwB_mailgate-MS-From: urban@ktilinux.ms.mff.cuni.cz X-UwB_mailgate-MS-To: mizar-forum@mizar.uwb.edu.pl x-spam-status: no Sender: owner-mizar-forum@mizar.uwb.edu.pl Precedence: bulk Reply-To: mizar-forum@mizar.uwb.edu.pl Hi, some first experimental applications and a description of the new Mizar XML format are now available. First version of semantically disambiguated complete Mizar articles linked to MML Query can be browsed at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html/ (more about them in the README file at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/). An experimental server running the eXist native XML database loaded with the MML resources (not proofs) can be queried at http://lipa.ms.mff.cuni.cz/~urban/existdemo.html . The server is quite fragile and aborts on queries taking longer than 1 second and too much memory. The description of these applications and Mizar XML-ization is at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/mizxml.ps . Comments are appreciated. Best, Josef Urban From owner-mizar-forum-outgoing@mizar.uwb.edu.pl Sun Apr 10 17:49:09 2005 Return-Path: X-Original-To: mizar-forum-outgoing Delivered-To: mizar-forum-outgoing@mizar.uwb.edu.pl Received: by mizar.uwb.edu.pl (Postfix, from userid 28) id 8D7A428641; Sun, 10 Apr 2005 17:49:05 +0200 (CEST) X-Original-To: mizar-forum@mizar.uwb.edu.pl Delivered-To: mizar-forum@mizar.uwb.edu.pl Received: from mailgate.uwb.edu.pl (mailgate.uwb.edu.pl [212.33.71.77]) by mizar.uwb.edu.pl (Postfix) with ESMTP id 5F2E71512F for ; Sun, 10 Apr 2005 17:49:05 +0200 (CEST) Received: from math.uwb.edu.pl (math.uwb.edu.pl [212.33.73.194]) by mailgate.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j3AFmwgp023493 for ; Sun, 10 Apr 2005 17:48:59 +0200 Received: from localhost (localhost [127.0.0.1]) by math.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j3AFmqGY011428 for ; Sun, 10 Apr 2005 17:48:52 +0200 (CEST) Date: Sun, 10 Apr 2005 17:48:52 +0200 (CEST) From: Adam Grabowski X-X-Sender: adam@math To: mizar-forum@mizar.uwb.edu.pl Subject: [mizar] New Mizar articles Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Virus-Scanned: by amavisd-new Received-SPF: pass (mailgate.uwb.edu.pl: domain of adam@math.uwb.edu.pl designates 212.33.73.194 as permitted sender) receiver=mailgate.uwb.edu.pl; client-ip=212.33.73.194; helo=math.uwb.edu.pl; envelope-from=adam@math.uwb.edu.pl; x-software=spfmilter 0.95 http://www.acme.com/software/spfmilter/ with libspf2; X-UwB_mailgate-MS-Information: Uniwersytet w Bialymstoku; e-mail: dask(at)uwb.edu.pl X-UwB_mailgate-MS: Found to be clean X-UwB_mailgate-MS-SpamCheck: not spam X-UwB_mailgate-MS-From: adam@math.uwb.edu.pl X-UwB_mailgate-MS-To: mizar-forum@mizar.uwb.edu.pl x-spam-status: no Sender: owner-mizar-forum@mizar.uwb.edu.pl Precedence: bulk Reply-To: mizar-forum@mizar.uwb.edu.pl Dear All, I would like to announce three new articles accepted to the Mizar Mathematical Library: 1. Stirling Numbers of the Second Kind by Karol P\c{a}k Received March 15, 2005 MML Id: STIRL2_1 2. Limit of Sequence of Subsets by Bo Zhang, Hiroshi Yamazaki and Yatsuka Nakamura Received March 15, 2005 MML Id: SETLIM_1 3. The Properties of Supercondensed Sets, Subcondensed Sets and Condensed Sets by Magdalena Jastrz\c{e}bska and Adam Grabowski Received March 31, 2005 MML Id: ISOMICHI Check our homepage http://mizar.uwb.edu.pl or its official mirror http://mizar.org for details. Regards, Adam Grabowski Library Committee of the Association of Mizar Users From owner-mizar-forum-outgoing@mizar.uwb.edu.pl Tue Apr 12 18:17:15 2005 Return-Path: X-Original-To: mizar-forum-outgoing Delivered-To: mizar-forum-outgoing@mizar.uwb.edu.pl Received: by mizar.uwb.edu.pl (Postfix, from userid 28) id B71242A425; Tue, 12 Apr 2005 18:17:10 +0200 (CEST) X-Original-To: mizar-forum@mizar.uwb.edu.pl Delivered-To: mizar-forum@mizar.uwb.edu.pl Received: from mailgate.uwb.edu.pl (mailgate.uwb.edu.pl [212.33.71.77]) by mizar.uwb.edu.pl (Postfix) with ESMTP id 8788D149FB for ; Tue, 12 Apr 2005 18:17:10 +0200 (CEST) Received: from math.uwb.edu.pl (math.uwb.edu.pl [212.33.73.194]) by mailgate.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j3CGH4sv005771 for ; Tue, 12 Apr 2005 18:17:06 +0200 Received: from [127.0.0.1] ([212.33.73.141]) by math.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j3CGGkdR020807 for ; Tue, 12 Apr 2005 18:16:53 +0200 (CEST) Message-ID: <425BF745.1020103@math.uwb.edu.pl> Date: Tue, 12 Apr 2005 18:28:53 +0200 From: Andrzej Trybulec User-Agent: Mozilla/5.0 (Windows; U; Win98; en-US; rv:1.7) Gecko/20040616 X-Accept-Language: en-us, en MIME-Version: 1.0 To: mizar-forum@mizar.uwb.edu.pl Subject: [mizar] [Fwd: Re: getting started with Mizar or some proof assistant] Content-Type: multipart/alternative; boundary="------------010803070002050306030708" X-Virus-Scanned: by amavisd-new Received-SPF: pass (mailgate.uwb.edu.pl: domain of trybulec@math.uwb.edu.pl designates 212.33.73.194 as permitted sender) receiver=mailgate.uwb.edu.pl; client-ip=212.33.73.194; helo=math.uwb.edu.pl; envelope-from=trybulec@math.uwb.edu.pl; x-software=spfmilter 0.95 http://www.acme.com/software/spfmilter/ with libspf2; X-UwB_mailgate-MS-Information: Uniwersytet w Bialymstoku; e-mail: dask(at)uwb.edu.pl X-UwB_mailgate-MS: Found to be clean X-UwB_mailgate-MS-SpamCheck: not spam X-UwB_mailgate-MS-From: trybulec@math.uwb.edu.pl X-UwB_mailgate-MS-To: mizar-forum@mizar.uwb.edu.pl x-spam-status: no Sender: owner-mizar-forum@mizar.uwb.edu.pl Precedence: bulk Reply-To: mizar-forum@mizar.uwb.edu.pl This is a multi-part message in MIME format. --------------010803070002050306030708 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Could somebody help him? A.T. -------- Original Message -------- Subject: Re: getting started with Mizar or some proof assistant Date: Mon, 11 Apr 2005 17:01:08 EDT From: Jasonc65@aol.com To: trybulec@math.uwb.edu.pl In a message dated 4/11/2005 6:44:20 AM Eastern Standard Time, trybulec@math.uwb.edu.pl writes: > You have first install Mizar. The address is: > > ftp://mizar.uwb.edu.pl/pub/system/current/ > > (where you live ? there are mirrors that may be better accessible for you) > > With the instalation you will get the Mizar mode for GNU Emacs. > I have already done that. That was what I was having trouble with. I'm getting cryptic errors having to do with path variables. And I can't find the autoexec.bat file in my computer and I forget where it goes. All attempts to set the variable have failed because none of them gave me a permanent shell that was in effect when the code was being executed. It is very frustrating having to search for files in rarely visited folders everytime I troubleshoot a software package that doesn't install from a wizard. I was the other day having trouble with the MIZPATH variable. The Mizar code for GNU Emacs simply isn't working on my system's present configuration and I have no clue how to fix it. I need foolproof instructions for in getting Mizar to work with Emacs now that they have been installed, including how to set up the .emacs file, the autoexec.bat file, the sytem variables, the Lisp functions, and everything else that needs to be set in order to make everything work. Then I will need some sample proof file to run and exactly what keys to press in Emacs to make it run. --------------010803070002050306030708 Content-Type: text/html; charset=us-ascii Content-Transfer-Encoding: 7bit Could somebody help him?

A.T.

-------- Original Message --------
Subject: Re: getting started with Mizar or some proof assistant
Date: Mon, 11 Apr 2005 17:01:08 EDT
From: Jasonc65@aol.com
To: trybulec@math.uwb.edu.pl 


In a message dated 4/11/2005 6:44:20 AM Eastern Standard Time, 
trybulec@math.uwb.edu.pl writes:

> You have first install Mizar. The address is:
> 
> ftp://mizar.uwb.edu.pl/pub/system/current/
> 
> (where you live ? there are mirrors that may be better accessible for you)
> 
> With the instalation you will get the Mizar mode for GNU Emacs.
> 

I have already done that.  That was what I was having trouble with.  I'm 
getting cryptic errors having to do with path variables.  And I can't find the 
autoexec.bat file in my computer and I forget where it goes.  All attempts to set 
the variable have failed because none of them gave me a permanent shell that 
was in effect when the code was being executed.  It is very frustrating having 
to search for files in rarely visited folders everytime I troubleshoot a 
software package that doesn't install from a wizard.  I was the other day having 
trouble with the MIZPATH variable.  The Mizar code for GNU Emacs simply isn't 
working on my system's present configuration and I have no clue how to fix it.  
I need foolproof instructions for in getting Mizar to work with Emacs now 
that they have been installed, including how to set up the .emacs file, the 
autoexec.bat file, the sytem variables, the Lisp functions, and everything else 
that needs to be set in order to make everything work.  Then I will need some 
sample proof file to run and exactly what keys to press in Emacs to make it run.
--------------010803070002050306030708-- From owner-mizar-forum-outgoing@mizar.uwb.edu.pl Tue Apr 12 18:27:12 2005 Return-Path: X-Original-To: mizar-forum-outgoing Delivered-To: mizar-forum-outgoing@mizar.uwb.edu.pl Received: by mizar.uwb.edu.pl (Postfix, from userid 28) id CCA4C2A542; Tue, 12 Apr 2005 18:27:07 +0200 (CEST) X-Original-To: mizar-forum@mizar.uwb.edu.pl Delivered-To: mizar-forum@mizar.uwb.edu.pl Received: from mailgate.uwb.edu.pl (mailgate.uwb.edu.pl [212.33.71.77]) by mizar.uwb.edu.pl (Postfix) with ESMTP id 9B33015215 for ; Tue, 12 Apr 2005 18:27:07 +0200 (CEST) Received: from izanagi.macs.hw.ac.uk (izanagi.macs.hw.ac.uk [137.195.13.5]) by mailgate.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j3CGR08s006193 for ; Tue, 12 Apr 2005 18:27:03 +0200 Received: from lxultra9.macs.hw.ac.uk ([137.195.27.159] ident=retel) by izanagi.macs.hw.ac.uk with esmtp (Exim 4.34) id 1DLOE2-0001Tn-30 for mizar-forum@mizar.uwb.edu.pl; Tue, 12 Apr 2005 17:26:54 +0100 Message-ID: <425BF6CD.70909@macs.hw.ac.uk> Date: Tue, 12 Apr 2005 17:26:53 +0100 From: Krzysztof Retel User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.3) Gecko/20040922 X-Accept-Language: en-us, en MIME-Version: 1.0 To: mizar-forum@mizar.uwb.edu.pl References: <425BF745.1020103@math.uwb.edu.pl> In-Reply-To: <425BF745.1020103@math.uwb.edu.pl> X-SA-Exim-Connect-IP: 137.195.27.159 X-SA-Exim-Mail-From: retel@macs.hw.ac.uk Subject: Re: [mizar] [Fwd: Re: getting started with Mizar or some proof assistant] Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Spam-Checker-Version: SpamAssassin 3.0.1 (2004-10-22) on izanagi X-Spam-Level: X-Spam-Status: No, score=0.0 required=7.0 tests=none autolearn=failed version=3.0.1, no X-SA-Exim-Version: 4.0 (built Tue, 14 Dec 2004 15:36:33 +0000) Received-SPF: none (mailgate.uwb.edu.pl: retel@macs.hw.ac.uk does not designate permitted sender hosts) receiver=mailgate.uwb.edu.pl; client-ip=137.195.13.5; helo=izanagi.macs.hw.ac.uk; envelope-from=retel@macs.hw.ac.uk; x-software=spfmilter 0.95 http://www.acme.com/software/spfmilter/ with libspf2; X-UwB_mailgate-MS-Information: Uniwersytet w Bialymstoku; e-mail: dask(at)uwb.edu.pl X-UwB_mailgate-MS: Found to be clean X-UwB_mailgate-MS-SpamCheck: not spam X-UwB_mailgate-MS-From: retel@macs.hw.ac.uk X-UwB_mailgate-MS-To: mizar-forum@mizar.uwb.edu.pl Sender: owner-mizar-forum@mizar.uwb.edu.pl Precedence: bulk Reply-To: mizar-forum@mizar.uwb.edu.pl > Could somebody help him? I've sent him an email. I hope I will help him. And I think that it will be better (first of all) to show him some examples that we were doing with our students. I will do that. Krzysztof > > -------- Original Message -------- > Subject: Re: getting started with Mizar or some proof assistant > Date: Mon, 11 Apr 2005 17:01:08 EDT > From: Jasonc65@aol.com > To: trybulec@math.uwb.edu.pl > > > >In a message dated 4/11/2005 6:44:20 AM Eastern Standard Time, >trybulec@math.uwb.edu.pl writes: > >> You have first install Mizar. The address is: >> >> ftp://mizar.uwb.edu.pl/pub/system/current/ >> >> (where you live ? there are mirrors that may be better accessible for you) >> >> With the instalation you will get the Mizar mode for GNU Emacs. >> > >I have already done that. That was what I was having trouble with. I'm >getting cryptic errors having to do with path variables. And I can't find the >autoexec.bat file in my computer and I forget where it goes. All attempts to set >the variable have failed because none of them gave me a permanent shell that >was in effect when the code was being executed. It is very frustrating having >to search for files in rarely visited folders everytime I troubleshoot a >software package that doesn't install from a wizard. I was the other day having >trouble with the MIZPATH variable. The Mizar code for GNU Emacs simply isn't >working on my system's present configuration and I have no clue how to fix it. >I need foolproof instructions for in getting Mizar to work with Emacs now >that they have been installed, including how to set up the .emacs file, the >autoexec.bat file, the sytem variables, the Lisp functions, and everything else >that needs to be set in order to make everything work. Then I will need some >sample proof file to run and exactly what keys to press in Emacs to make it run. > > > From owner-mizar-forum-outgoing@mizar.uwb.edu.pl Tue Apr 12 20:43:35 2005 Return-Path: X-Original-To: mizar-forum-outgoing Delivered-To: mizar-forum-outgoing@mizar.uwb.edu.pl Received: by mizar.uwb.edu.pl (Postfix, from userid 28) id 946F62A425; Tue, 12 Apr 2005 20:43:31 +0200 (CEST) X-Original-To: mizar-forum@mizar.uwb.edu.pl Delivered-To: mizar-forum@mizar.uwb.edu.pl Received: from mailgate.uwb.edu.pl (mailgate.uwb.edu.pl [212.33.71.77]) by mizar.uwb.edu.pl (Postfix) with ESMTP id 5B68615324 for ; Tue, 12 Apr 2005 20:43:31 +0200 (CEST) Received: from smtp2.ms.mff.cuni.cz (sns.ms.mff.cuni.cz [195.113.20.77]) by mailgate.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j3CIhN6k010764 for ; Tue, 12 Apr 2005 20:43:26 +0200 Received: from ktilinux.ms.mff.cuni.cz (ktilinux.ms.mff.cuni.cz [195.113.17.207]) by smtp2.ms.mff.cuni.cz (8.13.3/8.13.3) with ESMTP id j3CIhGTr046965 for ; Tue, 12 Apr 2005 20:43:17 +0200 (CEST) Received: from localhost (urban@localhost) by ktilinux.ms.mff.cuni.cz (8.11.6/linuxconf) with ESMTP id j3CHifu22475 for ; Tue, 12 Apr 2005 19:44:41 +0200 Date: Tue, 12 Apr 2005 19:44:41 +0200 (CEST) From: Josef Urban To: Subject: Re: [mizar] [Fwd: Re: getting started with Mizar or some proof assistant] In-Reply-To: <425BF6CD.70909@macs.hw.ac.uk> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Received-SPF: none (mailgate.uwb.edu.pl: urban@ktilinux.ms.mff.cuni.cz does not designate permitted sender hosts) receiver=mailgate.uwb.edu.pl; client-ip=195.113.20.77; helo=smtp2.ms.mff.cuni.cz; envelope-from=urban@ktilinux.ms.mff.cuni.cz; x-software=spfmilter 0.95 http://www.acme.com/software/spfmilter/ with libspf2; X-UwB_mailgate-MS-Information: Uniwersytet w Bialymstoku; e-mail: dask(at)uwb.edu.pl X-UwB_mailgate-MS: Found to be clean X-UwB_mailgate-MS-SpamCheck: not spam X-UwB_mailgate-MS-From: urban@ktilinux.ms.mff.cuni.cz X-UwB_mailgate-MS-To: mizar-forum@mizar.uwb.edu.pl x-spam-status: no Sender: owner-mizar-forum@mizar.uwb.edu.pl Precedence: bulk Reply-To: mizar-forum@mizar.uwb.edu.pl Just to have a clear answer here: 1. The MIZFILES variable has to be set before any work with Mizar. Using Emacs before the variable is set is useless. If not sure, test the Mizar installation first on command line with the "mizf" command, e.g.: "cp $MIZFILES/mml/abcmiz_0.miz .; mizf abcmiz_0" 2. The instruction for installation of the Emacs mode distributed with Mizar (file mizar.el) is in the beginning of that file (and yes, it could be placed in the Mizar README or INSTALL file): ;;; Usage ;; ;; If you obtained this with your Mizar distribution, just append ;; the .emacs file enclosed there to your .emacs. The default location of .emacs on Windows is described in the Emacs installation instructions at http://www.gnu.org/software/emacs/windows/faq3.html . Josef On Tue, 12 Apr 2005, Krzysztof Retel wrote: > > > Could somebody help him? > > I've sent him an email. I hope I will help him. > And I think that it will be better (first of all) to show him some > examples that we were doing with our students. > I will do that. > > Krzysztof > > > > > -------- Original Message -------- > > Subject: Re: getting started with Mizar or some proof assistant > > Date: Mon, 11 Apr 2005 17:01:08 EDT > > From: Jasonc65@aol.com > > To: trybulec@math.uwb.edu.pl > > > > > > > >In a message dated 4/11/2005 6:44:20 AM Eastern Standard Time, > >trybulec@math.uwb.edu.pl writes: > > > >> You have first install Mizar. The address is: > >> > >> ftp://mizar.uwb.edu.pl/pub/system/current/ > >> > >> (where you live ? there are mirrors that may be better accessible for you) > >> > >> With the instalation you will get the Mizar mode for GNU Emacs. > >> > > > >I have already done that. That was what I was having trouble with. I'm > >getting cryptic errors having to do with path variables. And I can't find the > >autoexec.bat file in my computer and I forget where it goes. All attempts to set > >the variable have failed because none of them gave me a permanent shell that > >was in effect when the code was being executed. It is very frustrating having > >to search for files in rarely visited folders everytime I troubleshoot a > >software package that doesn't install from a wizard. I was the other day having > >trouble with the MIZPATH variable. The Mizar code for GNU Emacs simply isn't > >working on my system's present configuration and I have no clue how to fix it. > >I need foolproof instructions for in getting Mizar to work with Emacs now > >that they have been installed, including how to set up the .emacs file, the > >autoexec.bat file, the sytem variables, the Lisp functions, and everything else > >that needs to be set in order to make everything work. Then I will need some > >sample proof file to run and exactly what keys to press in Emacs to make it run. > > > > > > > From owner-mizar-forum-outgoing@mizar.uwb.edu.pl Thu Apr 14 18:24:49 2005 Return-Path: X-Original-To: mizar-forum-outgoing Delivered-To: mizar-forum-outgoing@mizar.uwb.edu.pl Received: by mizar.uwb.edu.pl (Postfix, from userid 28) id C2FC128641; Thu, 14 Apr 2005 18:24:44 +0200 (CEST) X-Original-To: mizar-forum@mizar.uwb.edu.pl Delivered-To: mizar-forum@mizar.uwb.edu.pl Received: from mailgate.uwb.edu.pl (mailgate.uwb.edu.pl [212.33.71.77]) by mizar.uwb.edu.pl (Postfix) with ESMTP id 880DF15324 for ; Thu, 14 Apr 2005 18:24:44 +0200 (CEST) Received: from math.uwb.edu.pl (math.uwb.edu.pl [212.33.73.194]) by mailgate.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j3EGOX5M002463 for ; Thu, 14 Apr 2005 18:24:36 +0200 Received: from [127.0.0.1] ([212.33.73.141]) by math.uwb.edu.pl (8.12.11/8.12.11) with ESMTP id j3EGOJWo029308 for ; Thu, 14 Apr 2005 18:24:19 +0200 (CEST) Message-ID: <425E9C10.9080507@math.uwb.edu.pl> Date: Thu, 14 Apr 2005 18:36:32 +0200 From: Andrzej Trybulec User-Agent: Mozilla/5.0 (Windows; U; Win98; en-US; rv:1.7) Gecko/20040616 X-Accept-Language: en-us, en MIME-Version: 1.0 To: mizar-forum@mizar.uwb.edu.pl Subject: [mizar] [Fwd: Announcing SMT-COMP] Content-Type: multipart/alternative; boundary="------------050408010900040803060604" X-Virus-Scanned: by amavisd-new Received-SPF: pass (mailgate.uwb.edu.pl: domain of trybulec@math.uwb.edu.pl designates 212.33.73.194 as permitted sender) receiver=mailgate.uwb.edu.pl; client-ip=212.33.73.194; helo=math.uwb.edu.pl; envelope-from=trybulec@math.uwb.edu.pl; x-software=spfmilter 0.95 http://www.acme.com/software/spfmilter/ with libspf2; X-UwB_mailgate-MS-Information: Uniwersytet w Bialymstoku; e-mail: dask(at)uwb.edu.pl X-UwB_mailgate-MS: Found to be clean X-UwB_mailgate-MS-SpamCheck: not spam X-UwB_mailgate-MS-From: trybulec@math.uwb.edu.pl X-UwB_mailgate-MS-To: mizar-forum@mizar.uwb.edu.pl x-spam-status: no Sender: owner-mizar-forum@mizar.uwb.edu.pl Precedence: bulk Reply-To: mizar-forum@mizar.uwb.edu.pl This is a multi-part message in MIME format. --------------050408010900040803060604 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit -------- Original Message -------- Subject: Announcing SMT-COMP Date: Tue, 12 Apr 2005 17:08:58 -0400 (EDT) From: Clark Barrett To: barrett@cs.nyu.edu Please distribute. Apologies for multiple postings... =========================================================================== CAV'05 Satellite Event 1st International Satisfiability Modulo Theories Competition (SMT-COMP'05) Edinburgh, Scotland, UK July 6-10, 2005 CALL FOR BENCHMARKS CALL FOR ENTRANTS =========================================================================== Decision procedures for checking satisfiability of logical formulas are crucial for many verification applications. Of particular recent interest are solvers for Satisfiability Modulo Theories (SMT). SMT solvers decide logical satisfiability (or dually, validity) with respect to a background theory expressed in classical first-order logic with equality. The success of SMT for verification applications is largely due to the suitability of supported background theories for expressing verification conditions. Public competitions are a well-known means of stimulating advancement in software tools. For example, in automated reasoning, the CASC competition for first-order reasoning tools has seen steady improvement in the systems entered since the competition began in 1996. The SAT competition for propositional SAT solvers has also seen similar, sometimes dramatic, improvements from year to year. Exactly what role the competitions play in these improvements is hard to measure, but anecdotal evidence suggests that they act as a significant catalyst for tool implementors. SMT-COMP came out of discussions surrounding the SMT-LIB initiative at the 2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR) at IJCAR 2004. SMT-LIB is an initiative of the SMT community to build a library of SMT benchmarks in a proposed standard format. SMT-COMP will help serve this goal by contributing collected benchmark formulas used for the competition to the library, and by providing an incentive for implementors of SMT solvers to support the SMT-LIB format. The methodology and the results of the competition will be presented at the end of CAV, and a more detailed discussion of the competition will take place in a special session of the PDPAR workshop following CAV. --------------- Benchmarks --------------- The first SMT-COMP will feature benchmarks in the following problem divisions (these divisions correspond to SMT-LIB logics: see http://goedel.cs.uiowa.edu/smtlib/ for more details). * QF_UF (Uninterpreted Functions): This division consists of quantifier-free formulas whose satisfiability is to be decided modulo the empty theory. Each benchmark may introduce its own uninterpreted function and predicate symbols. * QF_IDL (Integer Difference Logic): This division consists of quantifier-free formulas to be tested for satisfiability modulo a background theory of integer arithmetic. The syntax of atomic formulas is restricted to difference logic, i.e. x - y op c, where op is either equality or inequality and c is an integer constant. * QF_RDL (Real Difference Logic): This division is like QF_IDL, except that the background theory is real arithmetic. * QF_UFIDL (Integer Difference Logic with Uninterpreted Functions): This division contains benchmarks in a logic which is similar to QF_IDL, except that it also allows uninterpreted functions and predicates. * QF_LIA (Linear Integer Arithmetic): This division consists of quantifier-free formulas to be tested for satisfiability modulo a background theory of integer arithmetic. The syntax of atomic formulas is restricted to contain only linear terms. * QF_LRA (Linear Real Arithmetic): This division is like QF_LIA, except that the background theory is real arithmetic. * QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions): This division contains benchmarks in a logic which is similar to QF_LIA, except that it also allows uninterpreted functions and predicates. * QF_UFLRA (Linear Real Arithmetic with Uninterpreted Functions): This division contains benchmarks in a logic which is similar to QF_LRA, except that it also allows uninterpreted functions and predicates. * QF_A (Non-extensional Arrays): Quantifier-free formulas over the theory of arrays without extensionality. * QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions and Arrays): This division consists of quantifier-free formulas to be tested for satisfiability modulo a background theory combining linear integer arithmetic, uninterpreted function and predicate symbols, and non-extensional arrays. * AUFLIA: (Linear Integer Arithmetic with Uninterpreted Functions and Arrays) This division consists of formulas with quantifiers to be tested for satisfiability modulo a background theory combining linear integer arithmetic, uninterpreted function and predicate symbols, and non-extensional arrays. We have collected an initial set of benchmarks in the SMT-LIB format, but we are looking for additional benchmarks in all divisions, (especially in QF_UF, QF_IDL, QF_A, and AUFLIA). If you have access to benchmarks in any of these divisions, even if they are not in the SMT-LIB format, please contact one of the organizers (see below). --------------- Solvers --------------- System pre-registration and submission is now open. Please refer to http://www.csl.sri.com/users/demoura/smt-comp/index.shtml for complete details on entering the competition. --------------- Important Dates --------------- Intent to Register: May 15, 2005 System Submission: June 20, 2005 Competition: July 6-10, 2005 ----------------- Organizers ----------------- Clark Barrett (New York University, barrett@cs.nyu.edu) Leonardo de Moura (SRI International, demoura@csl.sri.com) Aaron Stump (Washington University in St. Louis, stump@cse.wustl.edu) ---------------- More Information ---------------- For details on the competition, see http://www.csl.sri.com/users/demoura/smt-comp/index.shtml For more information on the smt-lib format, see http://goedel.cs.uiowa.edu/smtlib/ --------------050408010900040803060604 Content-Type: text/html; charset=us-ascii Content-Transfer-Encoding: 7bit

-------- Original Message --------
Subject: Announcing SMT-COMP
Date: Tue, 12 Apr 2005 17:08:58 -0400 (EDT)
From: Clark Barrett <barrett@cs.nyu.edu>
To: barrett@cs.nyu.edu 


Please distribute.  Apologies for multiple postings...

===========================================================================

                          CAV'05 Satellite Event

       1st International Satisfiability Modulo Theories Competition
                               (SMT-COMP'05)

                          Edinburgh, Scotland, UK
                              July 6-10, 2005

                            CALL FOR BENCHMARKS
                             CALL FOR ENTRANTS

===========================================================================

Decision procedures for checking satisfiability of logical formulas are crucial
for many verification applications. Of particular recent interest are solvers
for Satisfiability Modulo Theories (SMT). SMT solvers decide logical
satisfiability (or dually, validity) with respect to a background theory
expressed in classical first-order logic with equality. The success of SMT for
verification applications is largely due to the suitability of supported
background theories for expressing verification conditions.

Public competitions are a well-known means of stimulating advancement in
software tools. For example, in automated reasoning, the CASC competition for
first-order reasoning tools has seen steady improvement in the systems entered
since the competition began in 1996. The SAT competition for propositional SAT
solvers has also seen similar, sometimes dramatic, improvements from year to
year. Exactly what role the competitions play in these improvements is hard to
measure, but anecdotal evidence suggests that they act as a significant
catalyst for tool implementors.

SMT-COMP came out of discussions surrounding the SMT-LIB initiative at the 2nd
International Workshop on Pragmatics of Decision Procedures in Automated
Reasoning (PDPAR) at IJCAR 2004. SMT-LIB is an initiative of the SMT community
to build a library of SMT benchmarks in a proposed standard format.  SMT-COMP
will help serve this goal by contributing collected benchmark formulas used for
the competition to the library, and by providing an incentive for implementors
of SMT solvers to support the SMT-LIB format.

The methodology and the results of the competition will be presented at the end
of CAV, and a more detailed discussion of the competition will take place in a
special session of the PDPAR workshop following CAV.

---------------
Benchmarks
---------------

The first SMT-COMP will feature benchmarks in the following problem divisions
(these divisions correspond to SMT-LIB logics: see
http://goedel.cs.uiowa.edu/smtlib/ for more details).

* QF_UF (Uninterpreted Functions): This division consists of quantifier-free
  formulas whose satisfiability is to be decided modulo the empty theory. Each
  benchmark may introduce its own uninterpreted function and predicate symbols.

* QF_IDL (Integer Difference Logic): This division consists of quantifier-free
  formulas to be tested for satisfiability modulo a background theory of
  integer arithmetic.  The syntax of atomic formulas is restricted to
  difference logic, i.e. x - y op c, where op is either equality or inequality
  and c is an integer constant.

* QF_RDL (Real Difference Logic): This division is like QF_IDL, except that the
  background theory is real arithmetic.

* QF_UFIDL (Integer Difference Logic with Uninterpreted Functions): This
  division contains benchmarks in a logic which is similar to QF_IDL, except
  that it also allows uninterpreted functions and predicates.

* QF_LIA (Linear Integer Arithmetic): This division consists of quantifier-free
  formulas to be tested for satisfiability modulo a background theory of
  integer arithmetic.  The syntax of atomic formulas is restricted to contain
  only linear terms.

* QF_LRA (Linear Real Arithmetic): This division is like QF_LIA, except that
  the background theory is real arithmetic.

* QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions): This
  division contains benchmarks in a logic which is similar to QF_LIA, except
  that it also allows uninterpreted functions and predicates.

* QF_UFLRA (Linear Real Arithmetic with Uninterpreted Functions): This division
  contains benchmarks in a logic which is similar to QF_LRA, except that it
  also allows uninterpreted functions and predicates.

* QF_A (Non-extensional Arrays): Quantifier-free formulas over the theory
  of arrays without extensionality.

* QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays): This division consists of quantifier-free formulas to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and non-extensional
  arrays.

* AUFLIA: (Linear Integer Arithmetic with Uninterpreted Functions and Arrays)
  This division consists of formulas with quantifiers to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and non-extensional
  arrays.

We have collected an initial set of benchmarks in the SMT-LIB format, but we
are looking for additional benchmarks in all divisions, (especially in QF_UF,
QF_IDL, QF_A, and AUFLIA).  If you have access to benchmarks in any of these
divisions, even if they are not in the SMT-LIB format, please contact one of
the organizers (see below).

---------------
Solvers
---------------

System pre-registration and submission is now open.

Please refer to http://www.csl.sri.com/users/demoura/smt-comp/index.shtml for
complete details on entering the competition.

---------------
Important Dates
---------------

Intent to Register: May 15, 2005
System Submission: June 20, 2005
Competition: July 6-10, 2005

-----------------
Organizers
-----------------

Clark Barrett (New York University, barrett@cs.nyu.edu)
Leonardo de Moura (SRI International, demoura@csl.sri.com)
Aaron Stump (Washington University in St. Louis, stump@cse.wustl.edu)

----------------
More Information
----------------

For details on the competition, see
http://www.csl.sri.com/users/demoura/smt-comp/index.shtml

For more information on the smt-lib format, see
http://goedel.cs.uiowa.edu/smtlib/
--------------050408010900040803060604--