Formal Methods and Models -Section 002 - Spring 2013

Description

This course is an introduction to two kinds of formal systems - languages and logics - with important applications to computer science. The study of formal languages underlies important aspects of compilers and other language processing systems, as well as the theory of computation. Various systems of logic and automatic reasoning are put to use in artificial intelligence, database theory and software engineering. The entire course will give you practice in precise thinking and proof methods that play a role in the analysis of algorithms. The programming assignments in Lex and Prolog provide practical experience with some theoretical topics.

Course Outcomes

Will understand the concepts and relevance of logic, formal languages and automata theory, and computability .
Will be able to able to do mechanical formal proofs, program correctness proofs and solve problems in first-order logic.
Will be able to solve problems in elementary machine models: designing finite-state, pushdown and turing machines.
Will be able to solve problems in formal languages: writing regular expressions, regular grammars, and context-free grammars.

Textbook

Title: Logic and Languages Models for Computer Science
Authors: Henry Hamberger and Dana Richards
ISBN: 0-13-065487-6
Publisher: Prentice Hall

Class Details

Section 02:
Class Times: Monday, Wednesday 3.00-4.15
Location: Robinson Hall B208

Personnel

Instructor

Name: Duminda Wijesekera
Contact Email: dwijesek (at) gmu (dot) edu
Contact Phone: 703-993-5030
Office Hours: Mondays and Wednesdays 1.30 pm to 2.30 pm and by appt.
Office Location: Room 436, Research Building
Best way to reach me: email

Teaching Assistant

TA Name: Avramovic Ivan
TA Email: iavramo2 (at) gmu (dot) edu
Office hrs: TBD
Office Location: TBD

Syllabus

, , \hline\hline \hline

Topic	Week	Chapter/ Parts
Introduction	1	1
Propositional Logic and Proofs	1-2	2-3
Predicate Logic and Proofs	3-4	4-5
Applications: Prolog and Verification	5-6	6-7
Exam #1	6	1-7
Finite Automata, Regular Expressios	7-9	8-10
Lex: a Regular Expression Language	10	11
Context-Free Grammars & Applications	11-12	12-13
Turing Machines & Solvability	13-14	14

Grading

Quizzes	20%
Programs	20%
Exams	60%

The two exams, including the final, each cover about a half of the semester; the final is not cumulative. Of these exams the highest score will count 35%, and the lowest 25%.

Notes

The two exams, including the final, each cover about a half of the semester.
The final is not cumulative.
Of these exams the highest score will count 35%, and the lowest 25%.
Homework is ungraded.
Quizzes will test homework, typically every other class class.
The lowest quiz grades will be dropped.
There will be small programming assignments in Prolog and in Lex (or AWK).
All testing is closed book, but limited notes are permitted, as follows for exams (but not for quizzes). One sheet of notes (8.5 by 11 inches, 1 side only). NO COPYING is allowed. That means no photocopying of anything, even the textbook, though you may write out material from it verbatim. It also means no copying of anyone else's notes, even by hand. You may use a computer for editing your own notes. The sheet must be turned in with your exam. Violations of these rules for creating the notes is considered a violation of the Honor Code.

There is to be NO group work on the programs. Receiving direct contributions to the code that is submitted is considered a violation of the Honor Code. (See cs.gmu.edu/wiki/pmwiki.php/HonorCode for the GMU and Computer Science guidelines.)

Lateness

Programs will be marked down 25% each class they are late; in particular, it is marked down 25% after the due date.

IN ORDER TO GET A PASSING GRADE each student will also meet at least once with their academic advisor during the semester.

Honor Code
All violations are reported. GMU honor code