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

Sources

There are currently no sources for this slide.