Logic in CS

LectureNotes

Lesson 1

2017.9.11

Imperative Language

• Java , C/C++, Python

Declarative Language

• $L _ 1 = \left \{ x| x \% 2 = 0 \right \}$

Coq language :

What we have :

• ropositional logic
• Predicate logic
• Model checking
• Model logics

Grading

• Exame (Easy)

Chapter 1

Intro

• Propositional logic and natural deduction
• Propositional logic as a formal language : syntax and semantics
• Normal form
• SAT solvers

Declarative sentences

• In princple capable of being declared true/false.
• Formalization of declarative sentences.
• $\neg$ negation
• $\land$ conisjunction
• $\lor$ disjunction
• $\to$ implication

Natural deduction

• Page 5
• Colletion of proof rules.
• Infer formulas from other formulas
• $x \vdash y$ : y is provable form x.
• Sequent : $\phi_1 ,\phi_2,\dots \phi_n \vdash \psi$