OlliG
Current Slide
Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.
Introduction – Basic Notions
 A proof system is collection of inference rules of the form:


P _{ 1 } … P _{ n }
____________
C

where C is a conclusion sequent, and P _{ i } ‘s are premises sequents .
 If an infererence rule does not have any premises that are taken to be true (called an axiom ), its conclusion automatically holds.

Example:
Modus Ponens: From P, P → Q infer Q,
Universal instantiation: From (∀x)p(x) infer p(A)
 Theorems:
 Expressions that can be derived from the axioms and the rules of inference.
Speaker notes:
Content Tools
Tools
Sources (0)
Tags (0)
Comments (0)
History
Usage
Questions (0)
Playlists (0)
Quality
Sources
There are currently no sources for this slide.