Knowledge Systems Laboratory, Stanford
University
23
Electronic Circuit Domain Theory
uConnected terminals have the same signal
(=>
(Connected ?t1 ?t2)
(and
(Terminal ?t1) (Terminal
?t2) (= (Signal ?t1) (Signal
?t2))))
uRelation “Connected” is commutative
(<=> (Connected ?t1 ?t2) (Connected ?t2 ?t1))
uSignals are either on or off and only terminals have signals
(or (Signal ?x On) (Signal ?x Off) (Signal
?x ^))
(<=> (or
(Signal ?t On) (Signal ?t
Off)) (Terminal ?t))
(/= On
Off)
uA gate has at least 1 input terminal and 1 output terminal
(=> (Gate ?g) (and (Terminal (In ?g
1)) (Terminal (Out ?g 1))))