Electronic Circuit Domain Theory

• Connected terminals have the same signal

  (=> (Connected ?t1 ?t2) (Signal ?t1 (Signal ?t2)))
  
  (=> (Connected ?t1 ?t2) (= (Signal ?t1) (Signal ?t2)))
  

• Signal at terminal is either on or off

  (or (Signal ?t On) (Signal ?t Off))
  
  (not (= On Off))

• Connected is commutative

  (<=> (Connected ?t1 ?t2) (Connected ?t2 ?t1))
  

Previous slide

Next slide

Back to first slide

View graphic version