Lecture 1

What is logic

• A proof system where deductions can be made
• The semantics of things and how the truth/false value of an entity can be determined

Logic requirements

• Syntax
• Semantics
• Proof system

Logic syntax should be complete an the semantics should be sound.

Logic in action

Programming languages

• Syntax tells you what is allowed in a legitimate program
• Semantics tell you what the program will do

Databases

Database is a structured collection of logical records.

• Database query language: Language for asking questions about the logically structured data. E.g SQL

Formal methods

Thi is use of mathematically based methods to prove that programs have certain properties so that we don't have to rely on testing.

Model checking: Computer system modelled as a mathematical structure and then proving a property using the power of logic.

• Microprocessor design - Major microprocessor manufacturers still use model checking methods as part of their design process.
• Data communications protocol software - rapid prototyping systems use it to validate new data-communications
• Critical software - NASA uses model checking to make sure there aren't bugs in the space program code.
• Operating systems - Microsoft uses it to verify the correct functioning of new 

Hilbert's Programme

Hilbert at a quest to formalize Mathematics by saying that all mathematical statements could be written with a formal language and by manipulating things accoruding to formal rules. Then things could be proved with formalism.

The idea was to create an algorithm to prove things.

Gödel’s Incompleteness Theorems

He proved that in any logical system powerful enough to describe the arithmetic of the natural numbers then there are things which cannot be proved within the system. This was a devastating blow to hilbert.

Entscheidungsproblem

View count: 437