CALL FOR PARTICIPATION

CADE-15 Workshop on

Problem-solving Methodologies with Automated Deduction

Sunday, July, 5, 1998

[{*filter*}version included below ]

Recent examples have shown new practical applications of Automated

Deduction in various important domains. There are successes of

automated theorem provers (ATPs) in planning, demonstrating that ATPs

can even outperform specialised planning systems. In model-based

diagnosis, tableau-based proof procedures are used to compute

explanations of faulty circuits. In program verification, ATPs are

embedded to achieve a higher degree of automation. In systems to

support software reuse, ATPs are used to identify modules from a

library to match a given specification. In natural language

understanding ATP techniques are used to integrate world knowledge

into the interpretation process. Finally, the Robbins algebra success

demonstrated how automated theorem provers can continue to solve open

mathematical problems.

This workshop is intented to fall between a system competition and a

program consisting only of scientific talks. The workshop will

consider a set of examples, representative of different practical

domains, and analyse the effectiveness of different systems and

methodologies for solving each one.

Instead of measuring the raw power and speed of ATP systems over the

TPTP examples, we have a different focus: the solution of real-world

problems by ATP system designers plus their programs.

Submissions

-----------

The workshop home page

http://www.*-*-*.com/ ~peter/cade-15-ws/

contains problem sets from domains Mathematics, Software Verification,

Reactive Systems Specification, Natural Language Processing, Diagnosis

and Planning. Contributions may discuss one or more of these workshop

problems.

The paper to be submitted should consist of a description and analysis

of the whole solution process. That is, it should discuss:

o how the problem is formulated within the system (language/logic),

o which inference methods are used within the system,

o what, if any, user interaction is required,

o how the system parameters are tuned to find a solution, and

o how the solution is presented by the system.

Hopefully, some problems will be solved by more than one system.

Hence there will be a chance to compare solutions and to discuss the

differences between the proof systems and methods of attack.

Contributions dealing with a problem from the literature are also

welcome, provided that they discuss the solution process as proposed.

Contribution format:

Postscript, max. 10 pages llncs-style,

before May, 15.

The submissions will be reviewed by the organizers and accepted

contributions will be included into the workshop notes that will be

made available at the workshop.

Note: all workshop participants are expected to register for the main

CADE-15 conference.

Important Dates

---------------

Deadline for submissions: 15 May 1998

Notification of acceptance/rejection: 29 May 1998

Deadline for final text: 12 June 1998

Workshop: 5 July 1998

Organisers

----------

Information

-----------

or WWW: http://www.*-*-*.com/ ~cade-15/

or WWW: http://www.*-*-*.com/ ~peter/cade-15-ws/

or surface mail:

Peter Baumgartner

University of Koblenz-Landau

Institute for Computer Science

Rheinau 1

D-56075 Koblenz, Germany

Phone: +49-261-9119-426

Fax: +49-261-9119-496

\documentstyle{article}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Call for Participation %%

%% %%

%% CADE-Workshop on %%

%% %%

%% Problem Solving Methodologies %%

%% with Automated Deduction %%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\head{

{\bf CALL FOR PARTICIPATION

Quote:

}\\[2mm] Workshop on

\\[2mm]{\huge\bf Problem-solving Methodologies \\[1mm]

with Automated Deduction

Quote:

}\large\\[2mm] 5 July 1998

%

\\ in conjunction with

CADE-15

\\ Fif{*filter*}th International Conference on Automated Deduction

\\[3mm]

{\bf Lindau -- Germany

Quote:

}}

\def\body{

Recent examples have shown new practical applications of Automated

Deduction in various important domains. There are successes

of automated theorem provers (ATPs) in planning, demonstrating that

ATPs can even outperform specialised planning systems. In

model-based diagnosis, tableau-based proof procedures are used to

compute explanations of faulty circuits. In program verification, ATPs

are embedded to achieve a higher degree of automation. In systems to

support software reuse, ATPs are used to identify modules from a

library to match a given specification. In natural language

understanding ATP techniques are used to integrate world knowledge

into the interpretation process. Finally, the Robbins algebra

success demonstrated how automated theorem provers can continue to

solve open mathematical problems.

This workshop is intented to fall between a system competition and a

program consisting only of scientific talks. The workshop will

consider a set of examples, representative of different practical

domains, and analyse the effectiveness of different systems and

methodologies for solving each one.

Instead of measuring the raw power and speed of ATP systems over the

TPTP examples, we have a different focus: the solution of real-world

problems by ATP system designers plus their programs.

\sect{ SUBMISSIONS

Quote:

}

The workshop home page

{\tt http://www.*-*-*.com/ \~{}peter/cade-15-ws/}

contains problem sets from domains {\em Mathematics\/},

{\em Software Verification\/}, {\em Reactive Systems Specification\/},

{\em Natural

Language Processing\/}, {\em Diagnosis\/} and {\em

Planning\/}. Contributions may discuss one or more

of these workshop problems.

The paper to be submitted should consist of a description and analysis

of the whole solution process. That is, it should discuss:

\begin{itemize}

\item how the problem is formulated within the system (language/logic),

\item which inference methods are used within the system,

\item what, if any, user interaction is required,

\item how the system parameters are tuned to find a solution, and

\item how the solution is presented by the system.

\end{itemize}

Hopefully, some problems will be solved by more than one system.

Hence there will be a chance to compare solutions and to discuss the

differences between the proof systems and methods of attack.

Contributions dealing with a problem from the

literature are also welcome, provided that they discuss the solution

process as proposed.

{\em Contribution format:\/}

Postscript, max.\ 10 pages llncs-style,

{\bf before May, 15}.

The submissions will be reviewed by the organizers and accepted

contributions will be included into the

workshop notes that will be made available at the workshop.

{\em Note:\/} all workshop participants are expected to register for the main

CADE-15 conference.

\phantom{1}

Quote:

}

\long\def\pract{

\in{ORGANISERS:}{

\begin{itemize}

\item Peter Baumgartner \\ Universit{\"a}t Koblenz, Germany,\\

\item Ulrich Furbach \\ Universit{\"a}t Koblenz, Germany,\\

\item Michael Kohlhase \\ Universit{\"a}t des Saarlandes, Germany,\\

\item William McCune \\ Argonne National Laboratory, USA,\\

\item Wolfgang Reif \\ Universit{\"a}t Ulm, Germany,\\

\item Mark Stickel \\ SRI International, USA,\\

\item Tom{\'a}s Uribe \\ Stanford University, USA,\\

\end{itemize}

Quote:

}

\in{ IMPORTANT DATES

Quote:

}{\begin{center}

\info{ Deadline for submissions: }{15 May 1998}

\info{ Notification of acceptance/rejection:}{29 May 1998}

\info{ Deadline for final text: }{12 June 1998}

\info{ Workshop: }{5 July 1998}

\end{center}}

\in{ INFORMATION

Quote:

}{\begin{center}

\info {or WWW:}{ http://www.*-*-*.com/ .\\informatik.tu-darmstadt.de/\~{}cade-15/}

\info {or WWW:}{ http://www.*-*-*.com/ \~{}peter/cade-15-ws/}

\info {or surface mail:} {Peter Baumgartner

\\ University of Koblenz-Landau

\\ Institute for Computer Science

\\ Rheinau 1

\\ D-56075 Koblenz, Germany

\\

...

**read more »**