Sample Query

• Do inputs (On, On, Off) produce outputs (Off, On)?

• Prove:

  (=> (= (Signal (In 1 C1)) On)
  
  (= (Signal (In 2 C1)) On)
  (= (Signal (In 3 C1)) Off)
  (and (= (Signal (Out 1 C1)) Off) (= (Signal (Out 2 C1)) On)))

• Using the Deduction Theorem -

  • Assume: (= (Signal (In 1 C1)) On)
    (= (Signal (In 2 C1)) On)
    (= (Signal (In 3 C1)) Off)
  • Prove: (and (= (Signal (Out 1 C1)) Off)
    (= (Signal (Out 2 C1)) On)

Previous slide

Next slide

Back to first slide

View graphic version