Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: peter@mailhost.uni-koblenz.de
Message-Id: <m0plvlJ-0001rMC@mailhost.uni-koblenz.de>
Date: Wed, 30 Mar 94 10:38:50 +0200
To: fg121@inferenzsysteme.informatik.th-darmstadt.de, 
    rewriting-list@lorraine.loria.fr, theorem-provers@mc.lcs.mit.edu, 
    deduktion@intellektik.informatik.th-darmstadt.de, 
    adler@intellektik.informatik.th-darmstadt.de, kgs@csdec1.tuwien.ac.at, 
    aal@anu.edu.au, isabelle-users@cl.cam.ac.uk, info-hol@cs.uidaho.edu, 
    nqthm-users@cli.com, howe@research.att.com, clp@cis.ohio-state.edu
Subject: CFP (LAST): CADE Workshop `Theory Reasoning in Automated Deduction'

+---------------------------------------------------------------+
|								|
| 		    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}