Return-Path: Received: from CS.CMU.EDU by A.GP.CS.CMU.EDU id aa23192; 23 Sep 93 8:58:06 EDT Received: from swan.cl.cam.ac.uk by CS.CMU.EDU id aa15075; 23 Sep 93 8:57:40 EDT Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 23 Sep 1993 13:56:37 +0100 To: isabelle-users@cl.cam.ac.uk Subject: CADE-12: Calls for Workshops & Tutorials Date: Thu, 23 Sep 93 13:56:33 +0100 From: Lawrence C Paulson Message-ID: <"swan.cl.cam.:261390:930923125702"@cl.cam.ac.uk> Enclosed are the CADE-12 Calls for Workshops, Tutorials and Papers. Please distribute. Thank you. [ LaTeX, DVI and PostScript versions of these files are available by anonymous FTP from dream.dai.ed.ac.uk (192.41.104.168) in the directory /pub/cade-12. ] ----------------------------------------------------------------------- Twelfth International Conference on Automated Deduction Nancy, France Tutorials & Workshops: June 27 Conference: June 28-July 1, 1994 C A D E - 1 2 CALL FOR WORKSHOPS The CADE conferences are the major forum for the presentation of new research in all aspects of automated deduction. In conjunction with CADE-12 we hope to run several workshops. The workshops will be held, in parallel, on Monday 27th June and the main conference will be held from Tuesday 28th to Friday 1st July. Proposals for workshops are hereby solicited. CADE conferences cover all aspects of automated deduction: First vs. Higher Order Logics Classical vs. Non-Classical Logics Special vs. General Purpose Inference Interactive vs. Automatic Systems Specific topics of interest include (but are not limited to): Resolution Sequent Calculus Decision Procedures Unification Rewrite Rules Mathematical Induction and any applications of automated deduction, including: Deductive Databases Logic and Functional Programming Commonsense Reasoning Software and Hardware Development The CADE-12 workshops will be held at INRIA Lorraine and CRIN Campus Scientifique on Monday 27th June 1994. Following this the CADE-12 conference will be held at the Palais des Congr`es de Nancy, sponsored by CADE Inc. and hosted by INRIA and CRIN. Following CADE-12, the LICS-94 conference will be held in Paris, France from July 4-7, 1994. A sight-seeing trip to Dijon will link the two conferences. Anyone wishing to organise a workshop in conjunction with CADE-12 should write to the Programme Chair by 1st December 1993 describing the topic of the proposed workshop; explaining why this topic is relevant to CADE; naming the organisers and specifying the workshop's format and length. Further information about the arrangements for workshops and submission of papers can be obtained from the Programme Chair. Other information about the conference may be obtained from the Local Arrangements Chair. Programme Chair Local Arrangements Chair Alan Bundy Claude Kirchner Department of Artificial INRIA Lorraine & CRIN Intelligence Campus scientifique University of Edinburgh 615, rue du Jardin Botanique 80 South Bridge BP101 Edinburgh EH1 1HN 54602 Villers-les-Nancy CEDEX Scotland France Tel: [+44] 31-650-2716 Tel: [+33] 83 59 30 26 Fax: [+44] 31-650-6516 Fax: [+33] 83 27 83 19 Email: cade-12@ai.ed.ac.uk Email: cade-12@loria.fr ---------------------------------------------------------------------- Twelfth International Conference on Automated Deduction Nancy, France Tutorials & Workshops: June 27 Conference: June 28-July 1, 1994 C A D E - 1 2 CALL FOR TUTORIALS The CADE conferences are the major forum for the presentation of new research in all aspects of automated deduction. In conjunction with CADE-12 we plan to run several tutorials. The tutorials will be held, in parallel, on Monday 27th June and the main conference will be held from Tuesday 28th to Friday 1st July. Proposals for tutorials are hereby solicited. CADE conferences cover all aspects of automated deduction: First vs. Higher Order Logics Classical vs. Non-Classical Logics Special vs. General Purpose Inference Interactive vs. Automatic Systems Specific topics of interest include (but are not limited to): Resolution Sequent Calculus Decision Procedures Unification Rewrite Rules Mathematical Induction and any applications of automated deduction, including: Deductive Databases Logic and Functional Programming Commonsense Reasoning Software and Hardware Development The CADE-12 tutorials will be held at INRIA Lorraine and CRIN Campus Scientifique on Monday 27th June 1994. Following this the CADE-12 conference will be held at the Palais des Congr`es de Nancy, sponsored by CADE Inc. and hosted by INRIA and CRIN. Following CADE- 12, the LICS-94 conference will be held in Paris, France from July 4-7, 1994. A sight-seeing trip to Dijon will link the two conferences. Anyone wishing to give a tutorial in conjunction with CADE-12 should write to the Programme Chair by 1st December 1993 describing the topic of the proposed tutorial; explaining why this topic is relevant to CADE; naming the speakers and specifying the tutorial's length. The default length is 2 hours. Further information about the arrangements for tutorials, workshops and the submission of papers can be obtained from the Programme Chair. Other information about the conference may be obtained from the Local Arrangements Chair. Programme Chair Local Arrangements Chair Alan Bundy Claude Kirchner Department of Artificial INRIA Lorraine & CRIN Intelligence Campus scientifique University of Edinburgh 615, rue du Jardin Botanique 80 South Bridge BP101 Edinburgh EH1 1HN 54602 Villers-les-Nancy CEDEX Scotland France Tel: [+44] 31-650-2716 Tel: [+33] 83 59 30 26 Fax: [+44] 31-650-6516 Fax: [+33] 83 27 83 19 Email: cade-12@ai.ed.ac.uk Email: cade-12@loria.fr ---------------------------------------------------------------- The Twelfth International Conference on Automated Deduction Nancy, France June 28-July 1, 1994 CADE-12: Call for Papers The CADE conferences are the major forum for the presentation of new research in all aspects of automated deduction. Original research papers, descriptions of working reas- oning systems, and problem sets that provide innovative, challenging tests for automated reasoning systems, are solicited. CADE conferences cover all aspects of automated deduction: First vs. Higher Order Logics Classical vs. Non-Classical Logics Special vs. General Purpose Inference Interactive vs. Automatic Systems Specific topics of interest include (but are not limited to): Resolution Sequent Calculus Decision Procedures Unification Rewrite Rules Mathematical Induction and any applications of automated deduction, including: Deductive Databases Logic and Functional Programming Commonsense Reasoning Software and Hardware Development CADE-12 will be held at the Palais des Congres de Nancy and will be sponsored by CADE Inc. and hosted by INRIA and CRIN. Following CADE-12, the LICS-94 conference will be held in Paris, France from July 4-7, 1994. A sight-seeing trip to Dijon will link the two conferences. The Proceedings of CADE-12 will be published by Springer-Verlag in their Lecture Notes in Artificial Intelligence Series. Research papers should not exceed 15 (fifteen) proceedings pages. System descriptions and problem sets should not exceed 5 (five) proceedings pages. Springer style files should be used if possible; send an email with contents "HELP" to svserv@dhdspri6.bitnet. Alternatively, FTP anonymously from dream.dai.ed.ac.uk (see instructions in pub/cade-12/README). The title page of the submission should include the name, address (with email if possible) and telephone number of each author. Papers must be unpublished and not submitted for publication elsewhere. Submissions which are late, too long, or which require major revision, will not be considered. +-----------------------------------------------+ | Submission deadline: December 1, 1993 | | Notification of acceptance: February 14, 1994 | | Camera-ready copy due: March 29, 1994 | +-----------------------------------------------+ Authors should send 4 (four) copies of their submission to the Programme Chair. Further information about the conference may be obtained from the Local Arrangements Chair. Programme Chair Local Arrangements Chair Alan Bundy Claude Kirchner Department of Artificial INRIA Lorraine & CRIN Intelligence Campus scientifique University of Edinburgh 615, rue du Jardin Botanique 80 South Bridge BP101 Edinburgh EH1 1HN 54602 Villers-les-Nancy CEDEX Scotland France Tel: [+44] 31-650-2716 Tel: [+33] 83 59 30 26 Fax: [+44] 31-650-6516 Fax: [+33] 83 27 83 19 Email: cade-12@ai.ed.ac.uk Email: cade-12@loria.fr Return-Path: Received: from EDRC.CMU.EDU by A.GP.CS.CMU.EDU id aa24195; 28 Jan 94 7:47:56 EST Received: from swan.cl.cam.ac.uk by EDRC.CMU.EDU id aa24713; 28 Jan 94 7:46:02 EST Received: from mailhost.uni-koblenz.de (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 28 Jan 1994 12:43:16 +0000 Received: from bax.uni-koblenz.de by mailhost.uni-koblenz.de with smtp (Smail3.1.28.1) id m0pPsTG-0001caC; Fri, 28 Jan 94 13:38 MET Message-Id: Received: by bax.uni-koblenz.de (4.1/KO-2.0) id AA17847; Fri, 28 Jan 94 13:40:39 +0100 Date: Fri, 28 Jan 94 13:40:39 +0100 From: peter To: fg121@inferenzsysteme.informatik.th-darmstadt.de, cade-12@aisb.ed.ac.uk, rewriting-list@lorraine.loria.fr, theorem-provers@mc.lcs.mit.edu, deduktion@intellektik.informatik.th-darmstadt.de, kgs@logic.tuwien.ac.at, aal@anu.edu.au, isabelle-users@cl.cam.ac.uk, info-hol@cs.uidaho.edu, nqthm-users@cli.com Subject: CADE WS Theory reasoning +---------------------------------------------------------------+ | | | Call for Workshop Participation (CADE 12) | | | | | | THEORY REASONING IN AUTOMATED DEDUCTION | | | | | | Nancy, France, June 27, 1994 | | | +---------------------------------------------------------------+ [ LaTeX version included below ] Theory reasoning offers the possibility of combining general problem solving methods with specialized problem dependent rea- soning systems. A distinguished feature of theory reasoning sys- tems is that the interface for the interaction of the two reason- ing parts has to be designed very carefully. Examples of such calculi are theory resolution, theory model el- imination, and constraint resolution, where the combination of the two reasoners is done on the literal or formula level. Anoth- er approach offers unification based methods by integrating a specialized theory reasoner at the term level. Theory reasoning can also be seen as a framework for the integra- tion of different reasoning paradigms. The topic is of growing interest and is an example of semantics-based reasoning as op- posed to purely syntactic reasoning. Theory reasoning offers a bridge from powerful knowledge representation systems to effi- cient theorem proving. Topics of interest: -------------------- This workshop is intended to be quite broad; it should bring to- gether interested researchers to exchange ideas, clarify notions and point out new challenging research problems. Papers are wel- come on all aspects of theory reasoning, including, but not lim- ited to: o Applications of theory reasoning o Implementation issues o Computational aspects o Interface issues o Constraints o System descriptions o Hybrid systems o Theory reasoning calculi Workshop: ---------- The workshop is held in conjunction with CADE-12 (Twelth Interna- tional Conference on Automated Deduction). Attendence is by in- vitation only; authors of accepted papers will be invited. In- formal proceedings containing the accepted papers will be sup- plied by the CADE organizing committee. The registration will be by standard CADE registration forms. Further information about CADE-12 can be obtained by anonymous ftp from dream.dai.ed.ac.uk (192.41.104.168), directory /pub/cade-12. Submission: ------------ Potential participants should apply by submitting an abstract of about 5 pages to the address listed below. Please include your postal address, phone number and e-mail address. Although we ac- cept hardcopies we strongly prefer e-mail submissions. If possi- ble, please send compressed and uuencoded .dvi or .ps-files. Important dates: +-----------------------------------------------+ | Submission deadline: April 8, 1994 | | Notification of acceptance: April 29, 1994 | | Camera-ready copy due: May 20, 1994 | +-----------------------------------------------+ Address for submission and further questions: ---------------------------------------------- Ulrich Furbach University of Koblenz Dept. of Computer Science Rheinau 1 56075 Koblenz Germany Phone: +49 261 9119 433 Fax: +49 261 9119 499 uli@informatik.uni-koblenz.de Program Committee: ------------------- Peter Baumgartner Germany Hans-J"urgen B"urckert Germany Hubert Common France Alan Frisch UK Ulrich Furbach Germany Neil Murray USA Uwe Petermann Germany Mark Stickel USA %%%%%%%%%%%%%%%%%%%%%% LaTeX Version %%%%%%%%%%%%%%%%%%% \documentstyle[11pt]{article} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\headsep}{0.0in} \setlength{\textheight}{25cm} \pagestyle{empty} \setlength{\parindent}{0cm} \begin{document} \begin{center} {\LARGE Call for Workshop Participation (CADE 12)}\\[3ex] {\LARGE\bf Theory Reasoning in Automated Deduction} \\[3ex] {\large \bf Nancy, France, June 27, 1994} \end{center} \bigskip \parbox[t]{6.6cm}{ \setlength{\parskip}{0.5\baselineskip} {\bf Program Committee:}\\[0.5ex] \begin{tabular}{ll} Peter~Baumgartner & Germany\\ Hans-J{\"u}rgen~B{\"u}rckert & Germany\\ Hubert~Common & France\\ Alan~Frisch & UK\\ Ulrich~Furbach & Germany\\ Neil~Murray & USA\\ Uwe~Petermann & Germany\\ Mark~Stickel & USA \end{tabular} \bigskip {\bf Submission Address:}\\[0.5ex] \begin{tabular}{l} Ulrich~Furbach\\ University of Koblenz\\ Dept.\ of Computer Science\\ Rheinau 1\\ 56075 Koblenz\\ Germany\\[2mm] \hskip-0.5em\begin{tabular}[t]{ll} Phone: & +49~261~9119~433\\ Fax: & +49~261~9119~499\\ \multicolumn{2}{l}{\tt uli@informatik.uni-koblenz.de} \end{tabular}\\ \end{tabular} % } \hfill \rule[-10cm]{.3mm}{10.5cm} \hfill \parbox[t]{8.5cm}{ \setlength{\parskip}{0.5\baselineskip} {\bf Theory reasoning} offers the possibility of combining general problem solving methods with specialized problem dependent reasoning systems. A distinguished feature of theory reasoning systems is that the interface for the interaction of the two reasoning parts has to be designed very carefully. Examples of such calculi are theory resolution, theory model elimination, and constraint resolution, where the combination of the two reasoners is done on the literal or formula level. Another approach offers unification based methods by integrating a specialized theory reasoner at the term level. Theory reasoning can also be seen as a framework for the integration of different reasoning paradigms. The topic is of growing interest and is an example of semantics-based reasoning as opposed to purely syntactic reasoning. Theory reasoning offers a bridge from powerful knowledge representation systems to efficient theorem proving. }\\[2ex] {\bf Topics of interest:} This workshop is intended to be quite broad; it should bring together interested researchers to exchange ideas, clarify notions and point out new challenging research problems. Papers are welcome on all aspects of theory reasoning, including, but not limited to: \begin{quote} {\em \setlength{\tabcolsep}{2em} \begin{tabular}{ll} Applications of theory reasoning & Implementation issues\\ Computational aspects & Interface issues \\ Constraints & System descriptions\\ Hybrid systems & Theory reasoning calculi \end{tabular} } \end{quote} {\bf Workshop:} The workshop is held in conjunction with CADE-12 (Twelth International Conference on Automated Deduction). Attendence is by invitation only; authors of accepted papers will be invited. Informal proceedings containing the accepted papers will be supplied by the CADE organizing committee. The registration will be by standard CADE registration forms. Further information about CADE-12 can be obtained by anonymous ftp from {\tt dream.dai.ed.ac.uk} (192.41.104.168), directory {\tt /pub/cade-12}. \medskip {\bf Submission:} Potential participants should apply by submitting an {\bf abstract} of about {\bf 5 pages} to the address listed above. Please include your postal address, phone number and e-mail address. Although we accept hardcopies we {\em strongly\/} prefer {\bf e-mail submissions}. If possible, please send {\em compressed\/} and {\em uuencoded\/} $\star$.dvi or $\star$.ps-files. The {\bf deadline} for the submission is {\bf April 8, 1994}. {\bf Notification of acceptance} will be {\bf April 29, 1994}. {\bf Hardcopies} for the workshop abstracts are due {\bf May 20, 1994}. \end{document} %%%%%%%% End LaTeX Version %%%%%%%%%%%%%%%% ____________________________________________________________________ Peter Baumgartner | peter@infko.uni-koblenz.de University of Koblenz, | Institute for Computer Science | Voice: +49 261 9119-426 Rheinau 1, 56075 Koblenz, Germany | Fax: +49 261 9119-499 ____________________________________________________________________ From walsh@loria.fr Wed Feb 9 14:32:42 EST 1994 Article: 5560 of news.announce.conferences Xref: glinda.oz.cs.cmu.edu news.announce.conferences:5560 Newsgroups: news.announce.conferences Path: honeydew.srv.cs.cmu.edu!das-news.harvard.edu!noc.near.net!yale.edu!spool.mu.edu!howland.reston.ans.net!cs.utexas.edu!uunet!sparky!rick From: walsh@loria.fr (Toby Walsh) Subject: CFP: CADE-12 workshop on Automation of Proof by Mathematical Induction Message-ID: <1994Feb4.193710.9287@sparky.sterling.com> Sender: rick@sparky.sterling.com (Richard Ohnemus) Organization: CRIN & INRIA-Lorraine - Nancy - FRANCE Date: Fri, 4 Feb 1994 19:37:10 GMT Approved: rick@sparky.sterling.com Expires: Sat, 16 Apr 1994 08:00:00 GMT Lines: 259 X-Md4-Signature: 38d991298d65effe81790d07e8b1b1cd +---------------------------------------------------------------+ | | | Call for Participation | | | | CADE-12 Workshop on | | | | Automation of Proof by Mathematical Induction | | | | Nancy, France, Monday 27th June, 1994 | | | +---------------------------------------------------------------+ Mathematical induction is required for reasoning about objects or events containing repetition, e.g. computer programs with recursion or iteration, electronic circuits with feedback loops or parameterised components. It is thus a vital ingredient in the development of formal methods for the synthesis, verification and transformation of computer software and hardware. There are also applications of mathematical induction in the formation of plans containing repetition and in explanation based learning of repetitive actions. Thus the automation of inductive reasoning provides a major opportunity for the application of AI techniques to design problems in computer science. This workshop is the third in a series organised by the MInd and IndUS consortia on the automation of proofs by mathematical induction. Previous workshops were held in Albany (NY) in conjunction with CADE-11, and in Washington (DC) in conjunction with AAAI-93. MInd is a European consortium funded by ESPRIT and IndUS is a United States consortium funded by NSF. The workshop is open to both members and non-members of the MInd and IndUS consortia. Topics of interest: -------------------- The aim of the workshop is to bring together all researchers interested in automating inductive reasoning. Topics for discussion may include, but are not limited to, the following: o formalisms for inductive inference o explicit induction and inductive completion o architectures for inductive inference o heuristics for controlling inductive proof search o mechanisms for choosing induction rules o mechanisms for generalisation o mechanisms for suggesting lemmas o the productive use of failure o applications of inductive inference o the relationship between recursive programs and inductive proofs. You are invited to suggest other topics and possible speakers. Format of workshop: ------------------- The workshop will consist of panel discussions and research presentations. Each panel discussion will address a "hot topic" in inductive proof and will last approximately two hours. Two speakers, who have made rival and significant contributions to these topics, will each give a short introduction. The discussion will then be thrown open to the floor. A combination of technical and polemical contributions will be encouraged. So as to take advantage of the most recent developments, we will leave the final selection of "hot topics" until just before the workshop. Selected participants will be invited to give short presentations of their current research. Preference will be given to work that is novel, promising and not already familiar to the other participants. The workshop will be held in conjunction with CADE-12 (Twelth International Conference on Automated Deduction). Attendence is by invitation only. Registration will be via the standard CADE registration form. Further information about CADE-12 can be obtained by anonymous ftp from dream.dai.ed.ac.uk (192.41.104.168), directory /pub/cade-12. Submission: ------------ Persons wishing to attend the workshop should submit three copies of a 1 page summary of research in this area along with a postal address, phone number and an electronic mail address (if possible). Applications should be sent to Toby Walsh at the address below to arrive by Friday 15th April 1994. As postal services can be slow, we welcome electronic submissions, preferably in LaTeX or plain text format. All electronic submissions will be acknowledged on receipt (though submissions received before April 1st will not be acknowledged till after April 1st). The research summaries will be circulated to workshop participants. Important dates: +-----------------------------------------------+ | Submission deadline: April 15, 1994 | | Notification of acceptance: April 29, 1994 | +-----------------------------------------------+ Address for submission and any questions: ----------------------------------------- Toby Walsh IRST Loc. Pante di Povo I38100 Trento Italy Phone: (+39) 461 314359 Fax: (+39) 461 810851 Email: toby@irst.it Program Committee: ------------------- Alan Bundy, Edinburgh Michael Rusionwitch, Nancy Toby Walsh, Trento %%%%%%%%%%%%%%%%%%%%%% LaTeX Version %%%%%%%%%%%%%%%%%%% \documentstyle[11pt]{article} \setlength{\oddsidemargin}{0cm} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\headsep}{0.0in} \setlength{\textheight}{25cm} \pagestyle{empty} \setlength{\parindent}{0cm} \begin{document} \begin{center} {\LARGE Call for Workshop Participation (CADE 12)}\\[3ex] {\LARGE\bf Automation of Proof by Mathematical Induction} \\[3ex] {\large \bf Nancy, France, Monday 27th June, 1994} \end{center} \bigskip \parbox[t]{5.6cm}{ \setlength{\parskip}{0.5\baselineskip} ~ \\ {\bf Program Committee:}\\[2ex] \begin{tabular}{ll} Alan Bundy & Edinburgh \\ Michael Rusinowitch & Nancy \\ Toby Walsh & Trento \end{tabular} \bigskip {\bf Submission Address:}\\[2ex] \begin{tabular}{l} Toby Walsh \\ IRST \\ Loc. Pante di Povo \\ I38100 Trento \\ Italy \\[2mm] \hskip-0.5em\begin{tabular}[t]{ll} Phone: & (+39)~461~314359 \\ Fax: & (+39)~461~810851 \\ Email: & {\tt toby@irst.it} \end{tabular}\\ \end{tabular} % } \hfill \rule[-12cm]{.3mm}{12.5cm} \hfill \parbox[t]{8.5cm}{ \setlength{\parskip}{0.5\baselineskip} Mathematical induction is required for reasoning about objects or events containing repetition, e.g. computer programs with recursion or iteration, electronic circuits with feedback loops or parameterised components. It is thus a vital ingredient in the development of formal methods for the synthesis, verification and transformation of computer software and hardware. There are also applications of mathematical induction in the formation of plans containing repetition and in explanation based learning of repetitive actions. Thus the automation of inductive reasoning provides a major opportunity for the application of AI techniques to design problems in computer science. This workshop is the third in a series organised by the MInd and IndUS consortia on the automation of proofs by mathematical induction. Previous workshops were held in Albany (NY) in conjunction with CADE-11, and in Washington (DC) in conjunction with AAAI-93. MInd is a European consortium funded by ESPRIT and IndUS is a United States consortium funded by NSF. The workshop is open to both members and non-members of the MInd and IndUS consortia.}\\[2ex] {\bf Topics of interest:} The aim of the workshop is to bring together all researchers interested in automating inductive reasoning. Topics for discussion may include, but are not limited to, the following: %\begin{quote} {\em \setlength{\tabcolsep}{2em} \begin{tabular}{ll} formalisms for inductive inference & explicit induction and inductive completion \\ architectures for inductive inference & heuristics for controlling search \\ mechanisms for choosing induction rules & mechanisms for generalisation \\ mechanisms for suggesting lemmas & the productive use of failure \\ applications of inductive inference & relationship between recursion and induction \end{tabular} } %\end{quote} You are invited to suggest other topics and possible speakers. \medskip {\bf Format of Workshop:} The workshop will consist of panel discussions and research presentations. Each panel discussion will address a ``hot topic'' in inductive proof and will last approximately two hours. Two speakers, who have made rival and significant contributions to these topics, will each give a short introduction. The discussion will then be thrown open to the floor. A combination of technical and polemical contributions will be encouraged. So as to take advantage of the most recent developments, we will leave the final selection of ``hot topics'' until just before the workshop. Selected participants will be invited to give short presentations of their current research. Preference will be given to work that is novel, promising and not already familiar to the other participants. The workshop will be held in conjunction with CADE-12 (Twelth International Conference on Automated Deduction). Attendence is by invitation only. Registration will be via the standard CADE registration form. Further information about CADE-12 can be obtained by anonymous ftp from {\tt dream.dai.ed.ac.uk} (192.41.104.168), directory {\tt /pub/cade-12}. \medskip {\bf Submission:} Persons wishing to attend the workshop should submit three copies of a 1 page summary of research in this area along with a postal address, phone number and an electronic mail address (if possible). Applications should be sent to Toby Walsh at the address listed above to arrive by {\bf Friday 15th April 1994}. As postal services can be slow, we welcome electronic submissions, preferably in LaTeX or plain text format. All electronic submissions will be acknowledged on receipt (though submissions received before April 1st will not be acknowledged till after April 1st). The research summaries will be circulated to workshop participants. You will be notified of acceptance by {\bf Friday 29th April, 1994} at the latest. \end{document} %%%%%%%% End LaTeX Version %%%%%%%%%%%%%%%% From peter@uni-koblenz.de Wed Feb 9 14:34:05 EST 1994 Article: 5572 of news.announce.conferences Xref: glinda.oz.cs.cmu.edu news.announce.conferences:5572 Newsgroups: news.announce.conferences Path: honeydew.srv.cs.cmu.edu!fs7.ece.cmu.edu!europa.eng.gtefsd.com!uunet!sparky!rick From: peter@uni-koblenz.de (Peter Baumgartner) Subject: CFP: CADE 12 Workshop `Theory Reasoning in Automated Deduction' Message-ID: <1994Feb4.194900.11468@sparky.sterling.com> Sender: rick@sparky.sterling.com (Richard Ohnemus) Organization: University of Koblenz, Germany Date: Fri, 4 Feb 1994 19:49:00 GMT Approved: rick@sparky.sterling.com Expires: Sat, 9 Apr 1994 08:00:00 GMT Lines: 227 X-Md4-Signature: 6bd8ff64bfd5fd902ef8fbd9d3655aec +---------------------------------------------------------------+ | | | Call for Workshop Participation (CADE 12) | | | | | | THEORY REASONING IN AUTOMATED DEDUCTION | | | | | | Nancy, France, June 27, 1994 | | | +---------------------------------------------------------------+ [ LaTeX version included below ] Theory reasoning offers the possibility of combining general problem solving methods with specialized problem dependent rea- soning systems. A distinguished feature of theory reasoning sys- tems is that the interface for the interaction of the two reason- ing parts has to be designed very carefully. Examples of such calculi are theory resolution, theory model el- imination, and constraint resolution, where the combination of the two reasoners is done on the literal or formula level. Anoth- er approach offers unification based methods by integrating a specialized theory reasoner at the term level. Theory reasoning can also be seen as a framework for the integra- tion of different reasoning paradigms. The topic is of growing interest and is an example of semantics-based reasoning as op- posed to purely syntactic reasoning. Theory reasoning offers a bridge from powerful knowledge representation systems to effi- cient theorem proving. Topics of interest: -------------------- This workshop is intended to be quite broad; it should bring to- gether interested researchers to exchange ideas, clarify notions and point out new challenging research problems. Papers are wel- come on all aspects of theory reasoning, including, but not lim- ited to: o Applications of theory reasoning o Implementation issues o Computational aspects o Interface issues o Constraints o System descriptions o Hybrid systems o Theory reasoning calculi Workshop: ---------- The workshop is held in conjunction with CADE-12 (Twelth Interna- tional Conference on Automated Deduction). Attendence is by in- vitation only; authors of accepted papers will be invited. In- formal proceedings containing the accepted papers will be sup- plied by the CADE organizing committee. The registration will be by standard CADE registration forms. Further information about CADE-12 can be obtained by anonymous ftp from dream.dai.ed.ac.uk (192.41.104.168), directory /pub/cade-12. Submission: ------------ Potential participants should apply by submitting an abstract of about 5 pages to the address listed below. Please include your postal address, phone number and e-mail address. Although we ac- cept hardcopies we strongly prefer e-mail submissions. If possi- ble, please send compressed and uuencoded .dvi or .ps-files. Important dates: +-----------------------------------------------+ | Submission deadline: April 8, 1994 | | Notification of acceptance: April 29, 1994 | | Camera-ready copy due: May 20, 1994 | +-----------------------------------------------+ Address for submission and further questions: ---------------------------------------------- Ulrich Furbach University of Koblenz Dept. of Computer Science Rheinau 1 56075 Koblenz Germany Phone: +49 261 9119 433 Fax: +49 261 9119 499 uli@informatik.uni-koblenz.de Program Committee: ------------------- Peter Baumgartner Germany Hans-J"urgen B"urckert Germany Hubert Common France Alan Frisch UK Ulrich Furbach Germany Neil Murray USA Uwe Petermann Germany Mark Stickel USA %%%%%%%%%%%%%%%%%%%%%% LaTeX Version %%%%%%%%%%%%%%%%%%% \documentstyle[11pt]{article} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\headsep}{0.0in} \setlength{\textheight}{25cm} \pagestyle{empty} \setlength{\parindent}{0cm} \begin{document} \begin{center} {\LARGE Call for Workshop Participation (CADE 12)}\\[3ex] {\LARGE\bf Theory Reasoning in Automated Deduction} \\[3ex] {\large \bf Nancy, France, June 27, 1994} \end{center} \bigskip \parbox[t]{6.6cm}{ \setlength{\parskip}{0.5\baselineskip} {\bf Program Committee:}\\[0.5ex] \begin{tabular}{ll} Peter~Baumgartner & Germany\\ Hans-J{\"u}rgen~B{\"u}rckert & Germany\\ Hubert~Common & France\\ Alan~Frisch & UK\\ Ulrich~Furbach & Germany\\ Neil~Murray & USA\\ Uwe~Petermann & Germany\\ Mark~Stickel & USA \end{tabular} \bigskip {\bf Submission Address:}\\[0.5ex] \begin{tabular}{l} Ulrich~Furbach\\ University of Koblenz\\ Dept.\ of Computer Science\\ Rheinau 1\\ 56075 Koblenz\\ Germany\\[2mm] \hskip-0.5em\begin{tabular}[t]{ll} Phone: & +49~261~9119~433\\ Fax: & +49~261~9119~499\\ \multicolumn{2}{l}{\tt uli@informatik.uni-koblenz.de} \end{tabular}\\ \end{tabular} % } \hfill \rule[-10cm]{.3mm}{10.5cm} \hfill \parbox[t]{8.5cm}{ \setlength{\parskip}{0.5\baselineskip} {\bf Theory reasoning} offers the possibility of combining general problem solving methods with specialized problem dependent reasoning systems. A distinguished feature of theory reasoning systems is that the interface for the interaction of the two reasoning parts has to be designed very carefully. Examples of such calculi are theory resolution, theory model elimination, and constraint resolution, where the combination of the two reasoners is done on the literal or formula level. Another approach offers unification based methods by integrating a specialized theory reasoner at the term level. Theory reasoning can also be seen as a framework for the integration of different reasoning paradigms. The topic is of growing interest and is an example of semantics-based reasoning as opposed to purely syntactic reasoning. Theory reasoning offers a bridge from powerful knowledge representation systems to efficient theorem proving. }\\[2ex] {\bf Topics of interest:} This workshop is intended to be quite broad; it should bring together interested researchers to exchange ideas, clarify notions and point out new challenging research problems. Papers are welcome on all aspects of theory reasoning, including, but not limited to: \begin{quote} {\em \setlength{\tabcolsep}{2em} \begin{tabular}{ll} Applications of theory reasoning & Implementation issues\\ Computational aspects & Interface issues \\ Constraints & System descriptions\\ Hybrid systems & Theory reasoning calculi \end{tabular} } \end{quote} {\bf Workshop:} The workshop is held in conjunction with CADE-12 (Twelth International Conference on Automated Deduction). Attendence is by invitation only; authors of accepted papers will be invited. Informal proceedings containing the accepted papers will be supplied by the CADE organizing committee. The registration will be by standard CADE registration forms. Further information about CADE-12 can be obtained by anonymous ftp from {\tt dream.dai.ed.ac.uk} (192.41.104.168), directory {\tt /pub/cade-12}. \medskip {\bf Submission:} Potential participants should apply by submitting an {\bf abstract} of about {\bf 5 pages} to the address listed above. Please include your postal address, phone number and e-mail address. Although we accept hardcopies we {\em strongly\/} prefer {\bf e-mail submissions}. If possible, please send {\em compressed\/} and {\em uuencoded\/} $\star$.dvi or $\star$.ps-files. The {\bf deadline} for the submission is {\bf April 8, 1994}. {\bf Notification of acceptance} will be {\bf April 29, 1994}. {\bf Hardcopies} for the workshop abstracts are due {\bf May 20, 1994}. \end{document} %%%%%%%% End LaTeX Version %%%%%%%%%%%%%%%% -- ____________________________________________________________________ Peter Baumgartner | peter@infko.uni-koblenz.de University of Koblenz, | Institute for Computer Science | Voice: +49 261 9119-426 Rheinau 1, 56075 Koblenz, Germany | Fax: +49 261 9119-499 ____________________________________________________________________ From galmiche@loria.fr Mon Feb 14 19:14:22 EST 1994 Article: 20654 of comp.ai Xref: glinda.oz.cs.cmu.edu comp.ai:20654 Path: honeydew.srv.cs.cmu.edu!fs7.ece.cmu.edu!europa.eng.gtefsd.com!library.ucla.edu!agate!doc.ic.ac.uk!warwick!zaphod.crihan.fr!univ-lille1.fr!ciril.fr!muller!loria.fr!galmiche From: galmiche@loria.fr (Didier Galmiche) Newsgroups: comp.ai Subject: CFP: Proof search in type-theoretic languages Date: 12 Feb 1994 10:31:05 GMT Organization: CRIN & INRIA-Lorraine - Nancy - FRANCE Lines: 205 Distribution: world Message-ID: <2jib59$3u0@muller.loria.fr> NNTP-Posting-Host: fabert.loria.fr Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Call for Workshop Participation (CADE-12) PROOF SEARCH IN TYPE-THEORETIC LANGUAGES Nancy, France, June 26, 1994 This workshop will focus on the problems of proof search in type-theoretic languages. Such languages are used as logical frameworks for representing proofs and, in some cases, formalize connections between proofs and programs that support program synthesis. The purpose of the workshop is to discuss recent results in, and to establish and publicize a research agenda for, proof search in type theories and their use in the formal development of correct proofs and programs. Topics: ------ The workshop is intended to bring together researchers interested in all aspects of proof search in type-theoretic languages, including but not limited to the following topics: * foundations of proof search in type theory frameworks * techniques and concepts related to proof construction and related analysis * proof synthesis vs program synthesis (applications, specific methods) * environments for formal proof development in type-theoretic frameworks Workshop: -------- The workshop is held, during one full day (June 26, 1994), in conjunction with CADE-12 Conference). Attendance is by invitation only: authors of accepted submissions will be invited. Informal proceedings will be supplied by the CADE organizing committee. Submission: ---------- Researchers interested in presenting their work are invited to send an extended abstract (5-7 pages) to each of the organizers named below. Researchers interested in attending the workshop (without giving a presentation) should send a position paper (1-2 pages) presenting their interest. e-mail submissions (*.dvi or *.ps files) are requested (hardcopies are also accepted) before April 8, 1994. Notification of acceptance and invitations to the workshop will be issued by May 5, 1994. Material to be handed out at the workshop should be received in final form before May 24, 1994. All submissions and information requests should be sent to the workshop organizers: Didier Galmiche Lincoln Wallen CRIN-CNRS & INRIA Lorraine Computing Laboratory Campus Scientifique, B.P. 239 University of Oxford 54506 Vandoeuvre-les-Nancy, Parks Road, Oxford OX1 3QD, France U.K. email: Didier.Galmiche@loria.fr email: Lincoln.Wallen@prg.ox.ac.uk fax: [+33] 83 41 30 79 fax: [+44] 865 27 38 39 Deadlines --------- Deadline for submission: April 8, 1994 Notification of acceptance: May 5, 1994 Abstract final version: May 24, 1994 Program Committee: ------------------ D. Galmiche (CRIN-CNRS & INRIA, Nancy) L. Helmink (Philips Research Laboratories, Eindhoven) F. Pfenning (Carnegie Mellon University, Pittsburgh) S. Thompson (University of Kent) L. Wallen (University of Oxford) %%%%%%%%%%%%%%%%%%%%%% LaTeX Version %%%%%%%%%%%%%%%%%%% \documentstyle[11pt]{article} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\headsep}{0.0in} \setlength{\textheight}{25cm} \pagestyle{empty} \setlength{\parindent}{0cm} \begin{document} \begin{center} {\large \bf Call for Workshop Participation (CADE-12)}\\ ~\\ ~\\ {\LARGE \bf Proof search in type-theoretic languages}\\ ~\\ ~\\ {\large \bf Nancy, France, June 26, 1994} \end{center} ~\\ ~\\ This workshop will focus on the problems of proof search in type-theoretic languages. Such languages are used as logical frameworks for representing proofs and, in some cases, formalize connections between proofs and programs that support program synthesis. \\ The purpose of the workshop is to discuss recent results in, and to establish and publicize a research agenda for, proof search in type theories and their use in the formal development of correct proofs and programs.\\ ~\\ {\bf Topics:} The workshop is intended to bring together researchers interested in all aspects of proof search in type-theoretic languages, including, but not limited to, the following topics:\\ ~\\ \hspace*{10mm} $\bullet$ foundations of proof search in type theory frameworks \\ \hspace*{10mm} $\bullet$ techniques and concepts related to proof construction and related analysis \\ \hspace*{10mm} $\bullet$ proof synthesis vs program synthesis (applications, specific methods) \\ \hspace*{10mm} $\bullet$ environments for formal proof development in type-theoretic frameworks \\ ~\\ {\bf Workshop:} The workshop is held, during one full-day (June 26, 1994), in conjunction with CADE-12 Conference). Attendance is by invitation only: authors of accepted submissions will be invited. Informal proceedings will be supplied by the CADE organizing committee. \\ ~\\ {\bf Submission:} Researchers interested in presenting their work are invited to send an {\bf extended abstract (5-7 pages)} to each of the organizers named below. Researchers interested in attending the workshop (without giving a presentation) should send a position paper (1-2 pages) presenting their interest. {\bf e-mail submissions} ($\star$.dvi or $\star$.ps files) are requested (hardcopies are also accepted) before {\bf April 8, 1994}. Notification of acceptance and invitations to the workshop will be issued by {\bf May 5, 1994}. Material to be handed out at the workshop should be received in final form before {\bf May 24, 1994}. \\ ~\\ All submissions and information requests should be sent to the {\bf workshop organizers}: \begin{center} \begin{tabular}{l} Didier Galmiche \\ CRIN-CNRS $\&$ INRIA Lorraine \\ Campus Scientifique, B.P. 239 \\ 54506 Vand\oe uvre-l\`es-Nancy, France \\ email: Didier.Galmiche@loria.fr \\ fax: [+33] 83 41 30 79 \\ \end{tabular} \hspace*{2cm} \begin{tabular}{l} Lincoln Wallen \\ Computing Laboratory \\ University of Oxford \\ Parks Road, Oxford OX1 3QD, U.K. \\ email: Lincoln.Wallen@prg.ox.ac.uk \\ fax: [+44] 865 27 38 39 \end{tabular} \end{center} \begin{tabular}{l} {\bf Program Committee:}\\ D. Galmiche (CRIN-CNRS $\&$ INRIA, Nancy) \\ L. Helmink (Philips Research Laboratories, Eindhoven)\\ F. Pfenning (Carnegie Mellon University, Pittsburgh) \\ S. Thompson (University of Kent) \\ L. Wallen (University of Oxford) \\ \end{tabular} \hspace*{3mm} \begin{tabular}{l} {\bf Important dates}:\\ Submission due: \hspace*{17mm} April \hspace*{0.3mm} 8, 1994 \\ Notification of Acceptance: May \hspace*{1mm} 5, 1994 \\ Abstract final version: \hspace*{7mm} May 24, 1994 \\ \end{tabular} \end{document} %%%%%%%%%%%%%%%%%%%%%% END LaTeX Version %%%%%%%%%%%%%%%%%%% -- ============================================================================== = Didier GALMICHE = phone: (33) 83 59 20 15 = = CRIN-CNRS & INRIA Lorraine = fax: (33) 83 41 30 79 = = Batiment Loria, BP 239 = email: galmiche@loria.fr = = 54506 Vandoeuvre-les-Nancy = = = France = = ============================================================================== From galmiche@loria.fr Wed Mar 2 19:07:11 EST 1994 Article: 5694 of news.announce.conferences Xref: glinda.oz.cs.cmu.edu news.announce.conferences:5694 Newsgroups: news.announce.conferences Path: honeydew.srv.cs.cmu.edu!fs7.ece.cmu.edu!europa.eng.gtefsd.com!howland.reston.ans.net!cs.utexas.edu!uunet!sparky!rick From: galmiche@loria.fr (Didier Galmiche) Subject: CFP: Proof search in type-theoretic languages Message-ID: <1994Feb15.231144.16797@sparky.sterling.com> Sender: rick@sparky.sterling.com (Richard Ohnemus) Organization: CRIN & INRIA-Lorraine - Nancy - FRANCE Date: Tue, 15 Feb 1994 23:11:44 GMT Approved: rick@sparky.sterling.com Expires: Sat, 9 Apr 1994 08:00:00 GMT Lines: 206 X-Md4-Signature: 9b18ef0cf540c5e01be1c81c3f5ea7ee Call for Workshop Participation (CADE-12) PROOF SEARCH IN TYPE-THEORETIC LANGUAGES Nancy, France, June 26, 1994 This workshop will focus on the problems of proof search in type-theoretic languages. Such languages are used as logical frameworks for representing proofs and, in some cases, formalize connections between proofs and programs that support program synthesis. The purpose of the workshop is to discuss recent results in, and to establish and publicize a research agenda for, proof search in type theories and their use in the formal development of correct proofs and programs. Topics: ------ The workshop is intended to bring together researchers interested in all aspects of proof search in type-theoretic languages, including but not limited to the following topics: * foundations of proof search in type theory frameworks * techniques and concepts related to proof construction and related analysis * proof synthesis vs program synthesis (applications, specific methods) * environments for formal proof development in type-theoretic frameworks Workshop: -------- The workshop is held, during one full day (June 26, 1994), in conjunction with CADE-12 Conference). Attendance is by invitation only: authors of accepted submissions will be invited. Informal proceedings will be supplied by the CADE organizing committee. Submission: ---------- Researchers interested in presenting their work are invited to send an extended abstract (5-7 pages) to each of the organizers named below. Researchers interested in attending the workshop (without giving a presentation) should send a position paper (1-2 pages) presenting their interest. e-mail submissions (*.dvi or *.ps files) are requested (hardcopies are also accepted) before April 8, 1994. Notification of acceptance and invitations to the workshop will be issued by May 5, 1994. Material to be handed out at the workshop should be received in final form before May 24, 1994. All submissions and information requests should be sent to the workshop organizers: Didier Galmiche Lincoln Wallen CRIN-CNRS & INRIA Lorraine Computing Laboratory Campus Scientifique, B.P. 239 University of Oxford 54506 Vandoeuvre-les-Nancy, Parks Road, Oxford OX1 3QD, France U.K. email: Didier.Galmiche@loria.fr email: Lincoln.Wallen@prg.ox.ac.uk fax: [+33] 83 41 30 79 fax: [+44] 865 27 38 39 Deadlines --------- Deadline for submission: April 8, 1994 Notification of acceptance: May 5, 1994 Abstract final version: May 24, 1994 Program Committee: ------------------ D. Galmiche (CRIN-CNRS & INRIA, Nancy) L. Helmink (Philips Research Laboratories, Eindhoven) F. Pfenning (Carnegie Mellon University, Pittsburgh) S. Thompson (University of Kent) L. Wallen (University of Oxford) %%%%%%%%%%%%%%%%%%%%%% LaTeX Version %%%%%%%%%%%%%%%%%%% \documentstyle[11pt]{article} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\headsep}{0.0in} \setlength{\textheight}{25cm} \pagestyle{empty} \setlength{\parindent}{0cm} \begin{document} \begin{center} {\large \bf Call for Workshop Participation (CADE-12)}\\ ~\\ ~\\ {\LARGE \bf Proof search in type-theoretic languages}\\ ~\\ ~\\ {\large \bf Nancy, France, June 26, 1994} \end{center} ~\\ ~\\ This workshop will focus on the problems of proof search in type-theoretic languages. Such languages are used as logical frameworks for representing proofs and, in some cases, formalize connections between proofs and programs that support program synthesis. \\ The purpose of the workshop is to discuss recent results in, and to establish and publicize a research agenda for, proof search in type theories and their use in the formal development of correct proofs and programs.\\ ~\\ {\bf Topics:} The workshop is intended to bring together researchers interested in all aspects of proof search in type-theoretic languages, including, but not limited to, the following topics:\\ ~\\ \hspace*{10mm} $\bullet$ foundations of proof search in type theory frameworks \\ \hspace*{10mm} $\bullet$ techniques and concepts related to proof construction and related analysis \\ \hspace*{10mm} $\bullet$ proof synthesis vs program synthesis (applications, specific methods) \\ \hspace*{10mm} $\bullet$ environments for formal proof development in type-theoretic frameworks \\ ~\\ {\bf Workshop:} The workshop is held, during one full-day (June 26, 1994), in conjunction with CADE-12 Conference). Attendance is by invitation only: authors of accepted submissions will be invited. Informal proceedings will be supplied by the CADE organizing committee. \\ ~\\ {\bf Submission:} Researchers interested in presenting their work are invited to send an {\bf extended abstract (5-7 pages)} to each of the organizers named below. Researchers interested in attending the workshop (without giving a presentation) should send a position paper (1-2 pages) presenting their interest. {\bf e-mail submissions} ($\star$.dvi or $\star$.ps files) are requested (hardcopies are also accepted) before {\bf April 8, 1994}. Notification of acceptance and invitations to the workshop will be issued by {\bf May 5, 1994}. Material to be handed out at the workshop should be received in final form before {\bf May 24, 1994}. \\ ~\\ All submissions and information requests should be sent to the {\bf workshop organizers}: \begin{center} \begin{tabular}{l} Didier Galmiche \\ CRIN-CNRS $\&$ INRIA Lorraine \\ Campus Scientifique, B.P. 239 \\ 54506 Vand\oe uvre-l\`es-Nancy, France \\ email: Didier.Galmiche@loria.fr \\ fax: [+33] 83 41 30 79 \\ \end{tabular} \hspace*{2cm} \begin{tabular}{l} Lincoln Wallen \\ Computing Laboratory \\ University of Oxford \\ Parks Road, Oxford OX1 3QD, U.K. \\ email: Lincoln.Wallen@prg.ox.ac.uk \\ fax: [+44] 865 27 38 39 \end{tabular} \end{center} \begin{tabular}{l} {\bf Program Committee:}\\ D. Galmiche (CRIN-CNRS $\&$ INRIA, Nancy) \\ L. Helmink (Philips Research Laboratories, Eindhoven)\\ F. Pfenning (Carnegie Mellon University, Pittsburgh) \\ S. Thompson (University of Kent) \\ L. Wallen (University of Oxford) \\ \end{tabular} \hspace*{3mm} \begin{tabular}{l} {\bf Important dates}:\\ Submission due: \hspace*{17mm} April \hspace*{0.3mm} 8, 1994 \\ Notification of Acceptance: May \hspace*{1mm} 5, 1994 \\ Abstract final version: \hspace*{7mm} May 24, 1994 \\ \end{tabular} \end{document} %%%%%%%%%%%%%%%%%%%%%% END LaTeX Version %%%%%%%%%%%%%%%%%%% -- ============================================================================== = Didier GALMICHE = phone: (33) 83 59 20 15 = = CRIN-CNRS & INRIA Lorraine = fax: (33) 83 41 30 79 = = Batiment Loria, BP 239 = email: galmiche@loria.fr = = 54506 Vandoeuvre-les-Nancy = = = France = = ============================================================================== From peter@uni-koblenz.de Wed Mar 30 16:27:27 EST 1994 Article: 21421 of comp.ai Xref: glinda.oz.cs.cmu.edu comp.ai:21421 Path: honeydew.srv.cs.cmu.edu!nntp.club.cc.cmu.edu!news.mic.ucla.edu!library.ucla.edu!agate!howland.reston.ans.net!xlink.net!newshost.uni-koblenz.de!newshost!peter From: peter@uni-koblenz.de (Peter Baumgartner) Newsgroups: comp.ai Subject: CFP (LAST): CADE Workshop `Theory Reasoning in Automated Deduction' Date: 30 Mar 94 10:55:11 Organization: University of Koblenz, Germany Lines: 227 Message-ID: NNTP-Posting-Host: bax.uni-koblenz.de +---------------------------------------------------------------+ | | | 3rd (LAST) ANNOUNCEMENT | | | | Call for Workshop Participation | | | | | | THEORY REASONING IN AUTOMATED DEDUCTION | | | | | | held in conjunction with CADE-12 | | | | Nancy, France, June 27, 1994 | | | +---------------------------------------------------------------+ [ LaTeX version included below ] Theory reasoning offers the possibility of combining general problem solving methods with specialized problem dependent rea- soning systems. A distinguished feature of theory reasoning sys- tems is that the interface for the interaction of the two reason- ing parts has to be designed very carefully. Examples of such calculi are theory resolution, theory model el- imination, and constraint resolution, where the combination of the two reasoners is done on the literal or formula level. Anoth- er approach offers unification based methods by integrating a specialized theory reasoner at the term level. Theory reasoning can also be seen as a framework for the integra- tion of different reasoning paradigms. The topic is of growing interest and is an example of semantics-based reasoning as op- posed to purely syntactic reasoning. Theory reasoning offers a bridge from powerful knowledge representation systems to effi- cient theorem proving. Topics of interest: -------------------- This workshop is intended to be quite broad; it should bring to- gether interested researchers to exchange ideas, clarify notions and point out new challenging research problems. Papers are wel- come on all aspects of theory reasoning, including, but not lim- ited to: o Applications of theory reasoning o Implementation issues o Computational aspects o Interface issues o Constraints o System descriptions o Hybrid systems o Theory reasoning calculi Workshop: ---------- The workshop is held in conjunction with CADE-12 (Twelth Interna- tional Conference on Automated Deduction). Attendence is by in- vitation only; authors of accepted papers will be invited. In- formal proceedings containing the accepted papers will be sup- plied by the CADE organizing committee. The registration will be by standard CADE registration forms. Further information about CADE-12 can be obtained by anonymous ftp from dream.dai.ed.ac.uk (192.41.104.168), directory /pub/cade-12. Submission: ------------ Potential participants should apply by submitting an abstract of about 5 pages to the address listed below. Please include your postal address, phone number and e-mail address. Although we ac- cept hardcopies we strongly prefer e-mail submissions. If possi- ble, please send compressed and uuencoded .dvi or .ps-files. Important dates: +-----------------------------------------------+ | Submission deadline: April 8, 1994 | | Notification of acceptance: April 29, 1994 | | Camera-ready copy due: May 20, 1994 | +-----------------------------------------------+ Address for submission and further questions: ---------------------------------------------- Ulrich Furbach University of Koblenz Dept. of Computer Science Rheinau 1 56075 Koblenz Germany Phone: +49 261 9119 433 Fax: +49 261 9119 499 uli@informatik.uni-koblenz.de Program Committee: ------------------- Peter Baumgartner Germany Hans-J"urgen B"urckert Germany Hubert Common France Alan Frisch UK Ulrich Furbach Germany Neil Murray USA Uwe Petermann Germany Mark Stickel USA %%%%%%%%%%%%%%%%%%%%%% LaTeX Version %%%%%%%%%%%%%%%%%%% \documentstyle[11pt]{article} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\headsep}{0.0in} \setlength{\textheight}{25cm} \pagestyle{empty} \setlength{\parindent}{0cm} \begin{document} \begin{center} {\LARGE Call for Workshop Participation (CADE 12)}\\[3ex] {\LARGE\bf Theory Reasoning in Automated Deduction} \\[3ex] {\large \bf Nancy, France, June 27, 1994} \end{center} \bigskip \parbox[t]{6.6cm}{ \setlength{\parskip}{0.5\baselineskip} {\bf Program Committee:}\\[0.5ex] \begin{tabular}{ll} Peter~Baumgartner & Germany\\ Hans-J{\"u}rgen~B{\"u}rckert & Germany\\ Hubert~Common & France\\ Alan~Frisch & UK\\ Ulrich~Furbach & Germany\\ Neil~Murray & USA\\ Uwe~Petermann & Germany\\ Mark~Stickel & USA \end{tabular} \bigskip {\bf Submission Address:}\\[0.5ex] \begin{tabular}{l} Ulrich~Furbach\\ University of Koblenz\\ Dept.\ of Computer Science\\ Rheinau 1\\ 56075 Koblenz\\ Germany\\[2mm] \hskip-0.5em\begin{tabular}[t]{ll} Phone: & +49~261~9119~433\\ Fax: & +49~261~9119~499\\ \multicolumn{2}{l}{\tt uli@informatik.uni-koblenz.de} \end{tabular}\\ \end{tabular} % } \hfill \rule[-10cm]{.3mm}{10.5cm} \hfill \parbox[t]{8.5cm}{ \setlength{\parskip}{0.5\baselineskip} {\bf Theory reasoning} offers the possibility of combining general problem solving methods with specialized problem dependent reasoning systems. A distinguished feature of theory reasoning systems is that the interface for the interaction of the two reasoning parts has to be designed very carefully. Examples of such calculi are theory resolution, theory model elimination, and constraint resolution, where the combination of the two reasoners is done on the literal or formula level. Another approach offers unification based methods by integrating a specialized theory reasoner at the term level. Theory reasoning can also be seen as a framework for the integration of different reasoning paradigms. The topic is of growing interest and is an example of semantics-based reasoning as opposed to purely syntactic reasoning. Theory reasoning offers a bridge from powerful knowledge representation systems to efficient theorem proving. }\\[2ex] {\bf Topics of interest:} This workshop is intended to be quite broad; it should bring together interested researchers to exchange ideas, clarify notions and point out new challenging research problems. Papers are welcome on all aspects of theory reasoning, including, but not limited to: \begin{quote} {\em \setlength{\tabcolsep}{2em} \begin{tabular}{ll} Applications of theory reasoning & Implementation issues\\ Computational aspects & Interface issues \\ Constraints & System descriptions\\ Hybrid systems & Theory reasoning calculi \end{tabular} } \end{quote} {\bf Workshop:} The workshop is held in conjunction with CADE-12 (Twelth International Conference on Automated Deduction). Attendence is by invitation only; authors of accepted papers will be invited. Informal proceedings containing the accepted papers will be supplied by the CADE organizing committee. The registration will be by standard CADE registration forms. Further information about CADE-12 can be obtained by anonymous ftp from {\tt dream.dai.ed.ac.uk} (192.41.104.168), directory {\tt /pub/cade-12}. \medskip {\bf Submission:} Potential participants should apply by submitting an {\bf abstract} of about {\bf 5 pages} to the address listed above. Please include your postal address, phone number and e-mail address. Although we accept hardcopies we {\em strongly\/} prefer {\bf e-mail submissions}. If possible, please send {\em compressed\/} and {\em uuencoded\/} $\star$.dvi or $\star$.ps-files. The {\bf deadline} for the submission is {\bf April 8, 1994}. {\bf Notification of acceptance} will be {\bf April 29, 1994}. {\bf Hardcopies} for the workshop abstracts are due {\bf May 20, 1994}. \end{document} -- ____________________________________________________________________ Peter Baumgartner | peter@infko.uni-koblenz.de University of Koblenz, | Institute for Computer Science | Voice: +49 261 9119-426 Rheinau 1, 56075 Koblenz, Germany | Fax: +49 261 9119-499 ____________________________________________________________________