http:^^www.cs.uiowa.edu^~bonacina^22c:295.spring95.html

This data set contains WWW-pages collected from computer science departments of various universities

Date: Wed, 20 Nov 1996 23:17:33 GMT
Server: NCSA/1.5
Content-type: text/html

<TITLE>22C:295 Seminar in artificial intelligence - Spring 1995</TITLE>

<H1>22C:295 Seminar in artificial intelligence - Spring 1995</H1>
			
<H2>Parallelization of deduction strategies</H2>

<b> Instructor:</b>
<!WA0><A HREF="http://www.cs.uiowa.edu/~bonacina/">Maria Paola Bonacina</A>
([e-mail])

<p>
<b> Class meetings:</b> 10:55 - 12:10 TuTh in 422 Gilmore Hall

<p>
This course is an extension of the tutorial of the same title that the
instructor gave at the <em>Twelfth International Conference on Automated
Deduction (CADE)</em> in June 1994, Nancy, France,
and its background may be found in the paper<br>
<!WA1><A HREF="file://ftp.cs.uiowa.edu/pub/bonacina/papers/JAR94parallelism.ps.Z">
``Parallelization of deduction strategies: an analytical study''</A>,<br>
M. P. Bonacina and J. Hsiang,
<em><!WA2><A HREF="http://www.mcs.anl.gov/home/mccune/ar/jar/">
Journal of Automated Reasoning</A></em>, Vol. 13, 1-33, 1994.

<p>
<b> Contents of the course:</b>
The parallelization of deduction strategies is a research topic
which is becoming increasingly popular and important.
It combines knowledge from theorem proving, distributed systems,
parallel programming and distributed algorithms.
This course provides a systematic approach to this area at the
cross-road of several fields.
The course is organized as follows:

<ul>
<li> Deduction strategies
<ul>
<li> Basic definitions
<li> Survey of selected strategies as examples.
</ul>	
<li> A conceptual framework for parallel deduction
<ul>
<li> Classification of deduction strategies from the point of view
of parallelization;
<li> Types of parallelism for deduction;
<li> Presentation and discussion of relationships between classes of
strategies and types of parallelism.
</ul>	
<li> Survey and analysis of selected approaches to parallel deduction
including:
<ul>
<li> Prolog technology parallel theorem provers,
<li> Parallel resolution-based theorem provers,
<li> Parallel implementations of the Buchberger algorithm,
<li> Parallel implementations of Knuth-Bendix completion,
<li> Parallel contraction-based theorem provers.
</ul>	
<li> Analysis of the problems, suggestion and discussion of  solutions
<ul>
<li> What are the obstacles in effectively parallelizing
deduction strategies;
<li> How the choice of the deduction strategy, the type of architecture
and the type of parallel computation interact in determining the issues,
including e.g. size and degree of dynamicity of the data base
of clauses, shared memory versus distributed memory and
conflicts between parallel inferences;
<li> Focus on contraction-based strategies.
</ul>
</ul>

<!WA3><A HREF="http://www.cs.uiowa.edu/~bonacina/teaching.html">
Back to my teaching page.</A>

<HR>
<p>
This page was last updated on Monday, 13-May-96 11:47:40 CDT by
<!WA4><A HREF="http://www.cs.uiowa.edu/~bonacina/">Maria Paola Bonacina</A>
([e-mail]).