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
____________________________________________________________________