title: Circuit Verification using prolog
body: <p>i have been given functions and predicate to use to verify a 2 bit full adder circuit. This is what I have understood so far:-</p>
  
  <blockquote>
    <p>a function signal(t) where t is terminal and signal takes value 1 or 0.</p>
  </blockquote>
  
  <pre><code>signal(T, V) :- V is 1; V is 0.
  </code></pre>
  
  <blockquote>
    <p>a function type(x) where type is a circuit element and type(x) can take value xor, and, or</p>
  </blockquote>
  
  <pre><code>type(X, T) :- T is and; T is or; T is xor.
  </code></pre>
  
  <blockquote>
    <p>a function out(x) denoting output at gate x and in(n, x) n is an input terminal.</p>
  </blockquote>
  
  <pre><code>out(X, O) :- type(X, and), O is I1+I2, in(1, X, I1), in(1, X, I2). 
  %%and so on for other gates
  </code></pre>
  
  <blockquote>
    <p>for gates predicates are given as </p>
  </blockquote>
  
  <pre><code>forall X[{type(X) == OR} ----&gt; {(out(X) =1)}-----&gt; for some y(in(y, X) = 1)]
  </code></pre>
  
  <p>For these I am not sure how to convert them to prolog code and do not understand how prolog functions return something (I think the result must also be provided as a parameter).</p>
  
  <p>Any Help would be very useful ! </p>