From owner-theorynt@LISTSERV.NODAK.EDU Thu Mar 27 23:55:52 1997 Received: from CS.Stanford.EDU (CS.Stanford.EDU [171.64.64.64]) by robotics.Stanford.EDU (8.8.5/8.8.5) with ESMTP id XAA11218 for ; Thu, 27 Mar 1997 23:55:52 -0800 (PST) Received: from listserv.nodak.edu (listserv.NoDak.edu [134.129.111.8]) by CS.Stanford.EDU (8.8.4/8.8.4) with ESMTP id XAA06197; Thu, 27 Mar 1997 23:44:47 -0800 (PST) Received: from listserv (134.129.111.8) by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.6E46DBD0@listserv.nodak.edu>; Fri, 28 Mar 1997 1:43:27 -0600 Received: from LISTSERV.NODAK.EDU by LISTSERV.NODAK.EDU (LISTSERV-TCP/IP release 1.8c) with spool id 11524986 for THEORYNT@LISTSERV.NODAK.EDU; Fri, 28 Mar 1997 01:43:20 -0600 Received: from listserv (134.129.111.8) by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.6A1ABE50@listserv.nodak.edu>; Fri, 28 Mar 1997 1:43:20 -0600 Received: from LISTSERV.NODAK.EDU by LISTSERV.NODAK.EDU (LISTSERV-TCP/IP release 1.8c) with spool id 11524972 for THEORY-A@LISTSERV.NODAK.EDU; Fri, 28 Mar 1997 01:43:19 -0600 Received: from pollux.usc.edu by listserv.nodak.edu (LSMTP for Windows NT v1.1a) with SMTP id <0.65729300@listserv.nodak.edu>; Fri, 28 Mar 1997 1:43:12 -0600 Received: (from ierardi@localhost) by pollux.usc.edu (8.8.4/8.8.4/usc) id XAA06219 for theory-a@listserv.nodak.edu; Thu, 27 Mar 1997 23:43:10 -0800 (PST) Mime-Version: 1.0 (generated by tm-edit 7.69) Content-Type: text/plain; charset=US-ASCII Approved-By: Doug Ierardi Approved-By: Theory-A - TheoryNet World-Wide Events Message-ID: <199703261842.TAA23515@libellule.loria.fr> Date: Thu, 27 Mar 1997 23:43:10 PST Reply-To: strategy@loria.fr Sender: TheoryNet List From: Helene Kirchner Subject: CADE'14-Workshop on Strategies in AD Comments: To: THEORY-A@LISTSERV.NODAK.EDU To: THEORYNT@LISTSERV.NODAK.EDU X-Mozilla-Status: 0001 Content-Length: 3355 [ You may possibly receive this message multiple times. We sincerely apologize for the inconvenience.] CALL FOR PARTICIPATION CADE-14 WORKSHOP ON STRATEGIES IN AUTOMATED DEDUCTION ================================= July 13, 1997 Townsville, Australia http://www.loria.fr/~gramlich/cade14-ws-strategies.html MOTIVATIONS The concept of strategy allows describing and guiding computations and deductions in automated theorem provers, proof checkers, logical frameworks. Strategies are used for various purposes, e.g.: - proof search in theorem proving, - combination of different proof techniques and computation paradigms, - program transformation, - development of heuristics for playing games and finding proofs. Deterministic computations or inference rule based deductions are not sufficient to capture every computation or proof development. A mechanism is needed for instance to formalise the search for different solutions, the check of context conditions, the request for user input to instantiate variables, the processing of subgoals in a particular order. Strategies are used to guide application of rules, but may also involve iteration, case analysis, deterministic and non-deterministic choices. One may want to program strategies, to transform them, to prove some property on the computations or the proofs that they describe. AIMS The workshop aims at gathering different experiences on the use of strategies, under various terminology (tactic, tactical, method, heuristic, proof planning...), and in various application domains (first-order, higher-order, inductive theorem proving, program transformation, operational semantics...). Based on these experiments, we will address and discuss several points: - Strategy languages: Which basic constructs are needed? Expressiveness versus efficiency? Meta-language versus reflexivity? Higher-order versus first-order syntax? - Computational models for proof systems with strategies: Architecture, modularity of such systems? How to deal with user-interaction, input-output? - Verification of strategies: Which properties are required for strategies? Fairness, (partial) completeness, termination, etc.? How to ensure and/or check them? SUBMISSIONS Participants interested in presenting their work are invited to send an extended abstract (5-10 pages) by e-mail submission of a postscript file to the organizers (strategy@loria.fr) before April 21, 1997. Participants interested in attending the workshop without giving a presentation should send a position paper (1-2 pages) mentioning interest in one or several aspects of the topics. Additional information will be available through http://www.loria.fr/~gramlich/cade14-ws-strategies.html Attendance is by invitation only. Workshop registration is to be done as part of registration of CADE-14. The early registration deadline for CADE-14 is May 12, 1997. IMPORTANT DATES Deadline for submissions: April 21, 1997 position paper or abstract by e-mail Notification of acceptance: May 5,1997 Postcript version for proceedings: June 6,1997 Workshop: July 13, 1997 ORGANIZERS Bernhard Gramlich Helene Kirchner CRIN & INRIA-Lorraine (France) e-mail: strategy@loria.fr Fax: 33 3 83 27 83 19