Assignments

Thu Jan 18.
Skim [Ohl97], [Sti87] and [Hen00].
The first, [Ohl97], should be mostly review. The same for [Hen00] if you already know Prolog.

Tue Jan 23.
Continue reading [Ohl97], [Sti87] and [Hen00].
Read Chap. 2 of [Lei97] up to Theor. 2.3.1 included, skipping all proofs.

Fri Jan 26.
Review [Sti85] (to be presented by Jed).

Tue Jan 30.
Improve review of [Sti85] in light of what discussed on Friday.
(In class, we will finish going over the background material, briefly talk about Jed's presentation, and continue discussing [Sti85] .

Fri Feb 2.
Review [Bau92a] (to be presented by Tobias).

Tue Feb 6.
Review [Bau92b] (to be presented by David).

Fri Feb 9.
Figure out why factoring is not needed in partial theory resolution, assuming that the background reasoner accepts non-theory predicates.
Go over the previous papers thinking how you would implement the theory reasoning frameworks presented there. In particular, think of what exactly the tasks of the background reasoner and of foreground one should be.
Also, compare theory resolution with theory model elimination. What are the (dis)advantages of one with respect to the other?

Tue Feb 13.
Review [Bur94] (to be presented by Kirk).

Fri Feb 16.
Review [Fri91] (to be presented by Zijian).

Tue Feb 20.
Review [Baa99] (to be presented by Jed).

Fri Feb 23.
Go over [Bur94], [Fri91] and [Baa99] again, comparing the frameworks in each paper to each other. We will continue our discussion of the papers in class.

Tue Feb 27.
Review [Wan95] (to be presented by Tobias).

Fri Mar 2.
Review Part I (only) of [JafMah94] (to be presented by Kirk).

Tue Mar 6.
Review Part II of [JafMah94] (class discussion).

Fri Mar 9.
Review [TinHar98] (to be presented by Zijian).

Tue Mar 13.
No class.

Fri Mar 16.
No class.

Tue Mar 20.
Review [ArmRan98] (Constraint contextual rewriting, to be presented by David).

Fri Mar 23.
Review [ArmRan00].

Tue Mar 27.
Review [TinHar96]

Fri Mar 30.
Review [Cyr96]. To review this paper it may help to also take a look at reference [11] in [Cyr96]. If you don't already have one, a copy of that paper is available at my office.

Tue Apr 3.
Study in detail the congruence closure and the combination procedure pseudo-code in [Cyr96]. Compare the congruence closure code with the pseudo-code handed out in class last time.

Fri Apr 6.
Review the CC pseudo-code handed out in class in view of the changes we discussed on Tuesday. Rerun with the modified algorithm on the example seen in class on Tuesday. Study again the combination procedure pseudo-code in [Cyr96].

Tue Apr 10.
Review [BaaTin0?] ignoring Section 6 and 7 (to be presented by Cesare at 5pm in 3505 SC).

Fri Apr 13.
Class discussion on [BaaTin0?].

Tue Apr 17.
No class (moved to Thu, May 3).

Fri Apr 20.
Review [Bar96].

Tue Apr 24.
Continue reviewing [Bar96]

Fri Apr 27.
Review [Bec96].

Tue May 1.
Project presentation by Kirk and Tobias.

Thu May 3.
Project presentation by Jed.

Fri May 30.
Project presentation by Zijian and David.