Abstract

I will give a report on the current state of our NSF-DAAD cooperation with the Automated Reasoning Group at Saarbruecken and on the results of my Exchange Visit, February 4-8, 2002. In particular I will talk about some newly developed techniques for using proof planning to guide the developments of proofs in Nuprl. I will also talk about ActiveMath, a web-based learning environment that generates interactive mathematical courseware from OMDoc documents, and briefly summarize the results of other discussions with researchers at Saarbruecken.

The talk will involve a brief demo of the ActiveMath system and will therefore take place in 5126 Upson Hall

Slides:

[PS]