Online
Course web site:
http://sakura.cs.shinshu-u.ac.jp/pauline/course/ami/ami.html
Pauline N. Kawamoto, Ph.D.
Shinshu University,
Engineering Core Division, W1 Bldg. 6F Room 610, x5591
(026) 269-5591, +81-26-269-5591 (from outside Japan), pauline (at) cs.shinshu-u.ac.jp
Office Hours
|
Spring semesters
|
Thursdays, 15:00 - 17:00
|
|
Fall semesters
|
Tuesdays, 15:00 - 17:00
|
I am also available at other times by appointment.
Contents
Students will learn the basic notions and
techniques for formalizing concepts that can
be used to describe software and hardware
systems and study how to construct logical
proofs to verify specific conditions and characteristics
of the systems.
The main language for the course will be
English.
Prerequisites
The prerequisite skills for this class are:
- experience using the Web
- experience using e-mail
Familiarity with formalized languages helpful, but not required.
Objectives
At the end of the course, you should be able to:
- distinguish between mathematical definitions
and theorems
- sketch the outline of a proof (in natural language
and formalized language)
- begin the construction of a proof in a formalized
language
- discuss the differences between verifying
theorem proofs by humans and by machines.
Grading and Assignments
You will need to complete all of the exercises and
quizzes by the specified deadlines to be eligible for course credit.
Grading will be based on the completion of assignments/quizzes
(60%) and a final report (40%) demonstrating
the student's understanding of the differences between
proof checking done manually and mechanically.
Students will need a PC to do mechanical checking of
their proof texts before submssion to the instructor.
Related Reading
[1] Murata, T., "Petri Nets: Properties, Analysis and Applications", Proceedings of the IEEE,
Vol. 77, No. 4, April 1989.
