CS 228 : Logic for computer science 2020
Instructors : Ashutosh Gupta and
S. Krishna
Timings : 8:30 Monday, 9:30 Tuesday, 10:35 Thursday
Venue : CC103
TAs :
Riya Baviskar(170050011@),
Kalyani Dole (163050022@),
Tuppe Omkar Vijaykumar (omkarvtuppe@cse.),
Anuj Diwan (anujdiwan@cse.),
Aneesh Shetty(a3grand _at_ gmail.com),
Jatin Lamba (170050039.iitb _at_ gmail.com )
For non gmail email addresses Append "iitb.ac.in" in the text inside the parenthesis
Optional tutorials :
- Tutorial 1 : 2020-01-27T19:00@CC103 (Monday)
- Tutorial 2 : 2020-02-10T19:00@CC103 (Monday)
- Tutorial 3 : 2020-02-21T20:30@CC103 (Friday)
Source material
Evaluation structure
- Attendance: 5%
- Quizzes : 30% (4 quizzes)
- Midterm : 25% (2 hours)
- Final : 40% (3 hours)
May change later.
Attendance URL
View status of attendance
Tutorial problems
Lectures
Age of philosophy: propositional logic
2020-01-13 : Lecture 1 - Introduction
2020-01-14 : Lecture 2 - Propositional logic, syntax
2020-01-16 : Lecture 3 - Semantics and Truth tables
- Semantics, satisfiability problem, truth table, expressive power
- slides
Age of mathematics: formal proofs
2020-01-20 : Lecture 4 - Formal proofs
- derivations, proof rules
- slides
2020-01-21 : Lecture 5 - Formal proofs 2
- derived rules and soundness of proof system
- slides
Age of computer science: resolution proof system
2020-01-23 : Lecture 6 - Substitutions and equivalences
- Substitution theorem, and equivalences
- slides
2020-01-27 : Lecture 7 - Conjunctive normal forms
- Negation normal form, and conjunctive normal forms
- Tseitin's encoding, Disjunction normal forms
- slides
2020-01-28 : Lecture 8 - Low complexity SAT
- k-SAT, 3-SAT, 2-SAT, XOR-SAT
- Horn clauses
- slides
2020-01-29T08:30 (Wednesday) : Quiz 1@CC101,103,105
- You may bring a sheet of paper with the rules of the formal proof system.
- You may also include the 8 derived rules from lecture 5.
- Nothing else should be on your sheet.
2020-01-30 : Lecture 9 - Resolution
- Resolution proof system
- slides
2020-02-03 : Lecture 10 - Resolution completeness
- Completeness and compactness
- slides
Age of hacker : SAT solvers
2020-02-04 : Lecture 11 - SAT solvers
2020-02-06 : Lecture 12 - SAT encoding
- Encoding hard problems, Encoding bounds,
- slides
2020-02-08 (Saturday): Lecture 13 - Lab SAT solver
- Timing: 5PM-8PM
- Venue: SL1 and SL2 (at second floor of CC)
- Z3 will be installed in the lab machines!
- You may install in your own laptop before coming to the lab!
- slides
- Lab problems
- Z3 API
- Z3 installation instructions Linux Windows
For Windows:-
- Make sure python3 is installed.
- Open the following github link:- https://github.com/Z3Prover/z3.
- Open Releases
- Download z3-4.8.7-x64-win.zip
- Extract it and place the extracted folder to any desired destination.(e.g. C:\z3py\z3-4.8.7-x64-win)
- Now we have to set Environment Variables,
- Go to:- Control Panel > System and Security > System > Advanced system settings
- Select 'Advanced' tab and click on 'Environment Variables'
- In 'System Variable' section select variable with name 'Path' and click Edit button.
- Click on new button and paste the path of the 'bin' folder and press OK. (eg C:\z3py\z3-4.8.7-x64-win\bin)
- Click new in system variable section, write PYTHONPATH in Variable Name and paste the path of 'python' folder(eg C:\z3py\z3-4.8.7-x64-win\bin\python) which is located inside of 'bin' folder in Variable value. Press OK.
- Try to run example.py in the bin\python folder either through IDLE or cmd , it should not throw any error and give an output successfully.
- If the instructions do not work, contact the TA
For Linux:-
- Make sure python3 is installed.
- Open the following github link:- https://github.com/Z3Prover/z3.
- Open Releases
- Download
z3-4.8.7-x64-ubuntu-16.04.zip (or according to version of your ubuntu)
- Extract it.
- Open terminal and type following commands:-
(replace [BIN_PATH] with path of bin folder and [PYTHON_PATH] With path of python folder)
$export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:[BIN_PATH]
$export PYTHONPATH=[PYTHON_PATH]
Example :-
$export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:~/Downloads/z3-4.8.7-x64-ubuntu-16.04/bin
$export PYTHONPATH=~/Downloads/z3-4.8.7-x64-ubuntu-16.04/bin/python/
-
Try to run example.py in the bin\python folder , it should not throw any error and give an output successfully.
- To prevent resetting of path variables, type following command
gedit ~/.bashrc
Add both of above export lines to the end of file and save
- If the instructions do not work, contact the TA
First-Order Logic (FOL)
2020-02-10 : Lecture 14 - First-order logic - syntax
- Syntax, functions, predicates, terms, atoms, formulas
- sentences, closed terms, bounded and free variables
- slides
2020-02-11 : Lecture 15 - First-order logic - semantics
- Structures and assignments
- slides
2020-02-13 : Lecture 16 - Understanding FOL
- Examples and limits of FOL
- Substitututions and formal rules for the quantifiers
- slides
2020-02-15T(Saturday) : Quiz 2 @ SAT Solvers
- Timing: 09:00-12:00
- Venue: SL1 and SL2
2020-02-17 : Lecture 17 - Formal proofs
- Proof rules, derived rules, proving some properties of quantifiers
- slides
2020-02-18 : Lecture 18 - Unification
Attendance hacking challenge!
- Here is the source code of the attendance system
- If you can change your attendance by finding a flaw in the system, you will get the 5% of the attendance irrespective of your attendance.
- Ground rules: DO NOT TRY TO STEAL MY PASSWORD! Once you find a flaw, please report to me and do not share with others.
2020-02-20 : Lecture 19 - FOL CNF
2018-02-24 : Midterm week
- You may bring an A4 sheet of paper with the rules of the formal proof systems.
- You may also include the derived rules
- Nothing else should be on your sheet.
2020-03-02 : Lecture 20 - FOL Resolution
Lectures of second half
Lectures from 2020-03-03
- Slides will be availabe at Piazza