Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 1 Feb 1994 06:19:36 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA06490; Mon, 31 Jan 1994 23:10:25 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA06486; Mon, 31 Jan 1994 23:10:22 -0700 Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA05659; Mon, 31 Jan 1994 22:08:13 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.23) id AA02638; Mon, 31 Jan 94 22:08:04 -0800 Message-Id: <9402010608.AA02638@maui.cs.ucla.edu> To: info-hol@cs.uidaho.edu Subject: FWD: CADE-12 Workshop Date: Mon, 31 Jan 94 22:07:52 PST From: chou@cs.ucla.edu Begin forwarded message: From: Geoff Sutcliffe Subject: CADE-12 Workshop To: waldinger@ai.sri.com (Richard Waldinger), Mark.Wallace@ecrc.de (Mark Wallace), t.walsh@ed.ac.uk (Toby Walsh), XIISCWAS%DDATHD21.BITNET@relay1.uu.net (Christoph Walther), wang@kestrel.edu (T-C Wang), causun!dww@relay1.uu.net (Debora E. Weber-Wulff), weston@ucselx.sdsu.edu (Tom Weston), jgw@mitre.org (James G. Williams), wos@mcs.anl.gov (Larry Wos), graham@sol.newcastle.edu.au (Graham Wrightson), xin@herky.cs.uiowa.edu (Gary Hua Xin), shirai@icot.or.jp (Shirai Yasuyuki), yelick@cs.berkeley.edu (Katherine Yelick), hzhang@cs.uiowa.edu (Hantao Zhang), deduktion@intellektik.informatik.th-darmstadt.de (German Deduction Group Zx), setheo@informatik.tu-muenchen.de, wir+@sunjessen16.informatik.tu-muenchen.de, theorem-provers@ai.mit.edu (MIT AI list Zx), 100015.233@compuserve.com, J.F.Groote@cwi.nl, arun@mesa2.mesa.colorado.edu, brodsky%nhu.uucp@yale.edu, cowles@corral.uwyo.edu, eliens@cs.vu.nl, gbrownb@cix.compulink.co.uk, gumb@hawk.uml.edu, hjb@dfki.uni-sb.de, hlb@uafhp.uark.edu, jim@filly.calstate.edu, jvaj@linus.mitre.org, kalman@mat.aukuni.ac.nz, kohlhase@cs.uni-sb.de, maabhya%indst.BITNET@relay1.uu.net, minor@cs.unlv.edu, rbaum@gmuvax.gmu.edu, schauss@informatik.uni-frankfurt.de, shindhelm%wkuvx1.BITNET@relay1.uu.net, smithb%dayton.BITNET@relay1.uu.net, uw@decum.enet.dec.com, aal@anu.edu.au (Australiasian Association for Logic Zx), dahlhaus@cs.su.oz.au (Elias Dahlhaus), simon@cs.su.oz.au (Simon Dixon), dfs@hilbert.maths.utas.edu.au (Desmond Fearney-Sander), norman@cs.su.oz.au (Norman Foo), markg@arp.anu.edu.au (Mark Grundy), richard@cit.gu.edu.au (Richard Hagen), rkwok@cs.su.oz.au (Rex Kwok), BLow@coral.cs.jcu.edu.au, DMeagher@coral.cs.jcu.edu.au, TMinami@coral.cs.jcu.edu.au, abhaya@karl.cs.su.oz.au (Abhaya Nayak), nowak@cs.adelaide.edu.au (Chris Nowak), tyrone@cs.su.oz.au (Tyrone O'Neill), kimba@st.nepean.uws.edu.au (Michael Newton), morri@cs.su.oz.au (Maurice Pagnucco), purple@cs.su.oz.au (Matthew Partridge), anand@aaii.oz.au (Anand Rao), RRiley@coral.cs.jcu.edu.au, sattar@cit.gu.edu.au (Abdul Sattar), larry@cit.gu.edu.au (Larry Stewart-Zerba), maryanne@frey.newcastle.edu.au (Mary-anne Williams), yan@cs.su.oz.au (Yan Zhang), igpl-re@CS.UCLA Date: Tue, 1 Feb 1994 08:26:06 +1000 (+1000) X-Mailer: ELM [version 2.4 PL23] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 4500 CALL FOR WORKSHOP PARTICIPATION CADE-12 Workshop on Evaluation of Automated Theorem Proving Systems ----------------------------------------------- June 27, 1994 Nancy, France Currently, ATP system evaluations are often done in an ad hoc fashion, by testing the system on a small number of arbitrary (or advantageously) selected problems. At best, such an evaluation shows only that there exist cases where the system performs well. It does not show that the system (or a specific technique) is of general significance. In order to improve the status quo, it is important for the ATP community to address the following questions: * What are ATPs (intended to be) good for in the foreseeable future? - What is their 'real' expected work profile? - What are their required abilities? - Who are potential users? * What are the aims and expectations of an ATP system evaluation? Do we only want to know the refutation performance? ATP system evaluation may also wish to expose other properties of the system; what properties should be exposed? * What performance measures are appropriate for which systems? - In sequential systems, time and number of inferences to complete proofs are the common measures. Are these appropriate? Other issues include : + Completeness and soundness + Range of logics that can be processed + Software quality (portability, modularity, interfaces, ...) - The evaluation of parallel systems is more complex. What measures are appropriate there? How should parallel systems be compared with sequential ones? - How can interactive ATP systems be compared with fully automated ones? * Which properties should test problems have? - Should test problems reflect the expected 'real' work profile? Or should we be concerned with an ability to deal with all pathological cases? - What needs to be in a benchmark suite for ATPs? * How should an ATP system evaluation be performed? - Is it possible to define a framework within which everyone should work? - Is it possible to give a quantitative measure of system quality? - How should the performance measures be presented? - How should ATP systems be compared? - How can the difficulty of a given problem be measured? The aim of the workshop is to bring together researchers who have, or are interested in, methods, results, and conclusions that help answer the above questions. Through the presentation and discussion of relevant ideas, progress towards formal and appropriate ATP system evaluation can be made. Contributions that provide input to these issues are invited. Some answers to the questions may have already been found in existing ATP system evaluations. The workshop is thus an appropriate forum for the presentation of system evaluations, with the emphasis on the evaluation technique, rather than the ATP system itself. Specific performance measures, test problems, measures of ATP work profiles, and evaluation schemes, are all of interest. Contributions that describe such pragmatic results are also invited. Please submit a copy of either an extended abstract (3-4 pages) or a full paper to each of the organizers named below (email submissions are acceptable). Researchers interested in attending workshop, but who do not want to give a presentation, should submit a (1 page) position paper explaining their interest. Accepted submissions will be made available as proceedings at the day of the workshop (this will not preclude formal publication of the material elsewhere). Deadlines ~~~~~~~~~ Submissions due: April 8, 1994 Notification of Acceptance: May 5, 1994 Camera-ready version due: May 20, 1994 Fees ~~~~ CADE-12 will charge a marginal fee for participation. Registration to the main conference will not be mandatory. Organizers ~~~~~~~~~~ Christian B. Suttner Geoff Sutcliffe Institut f"ur Informatik Department of Computer Science TU M"unchen James Cook University D-80290 M"unchen, Germany Townsville, Queensland, Australia, 4811 suttner@informatik.tu-muenchen.de geoff@cs.jcu.edu.au phone: +49-89-521098 phone: +61-77-814622 fax : +49-89-526502 fax : +61-77-814029