Lab for Automated Reasoning and Analysis LARA

Lecture 01: Introduction and Background

Background

Propositional Logic Informally - Propositional Logic is the core logical reasoning

Predicate Logic Informally - We build on propositional logic from last lecture to explain first-order predicate logic.

Proofs and Induction - We make sure that we are all familiar with basic proof techniques, which we will study as formal rule systems later.

Theorem Prover - Theorem provers can check proofs, automate the proof search or use other methods to show formula validity.

Computational Complexity - Limits of algorithms for theorem provers and decision procedures, and vocabulary for expressing problem difficulty.

Compiler - Compilers help us understand how to deploy verification systems (see also our Compiler Construction course)

Sets and Relations - Some more background, useful preparation for program semantics.

(Continued in Lecture 02)

 
sav09/lecture_01.txt · Last modified: 2010/02/21 21:24 by vkuncak
 
© EPFL 2018 - Legal notice