title: Representing inference rules in z3
body: <p>I have been reading and working through several pieces of documentation and I'm still unclear on how to represent my inference rules in z3.</p>
  
  <p>Let's say I have the following 2 inference rules:</p>
  
  <p><a href="https://i.stack.imgur.com/QmpKn.jpg" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/QmpKn.jpg" alt="toy inference rules for question"></a></p>
  
  <p>Is it so simple that my z3 rules will be:</p>
  
  <p>a. <code>(a ^ b) =&gt; c</code><br>
   b. <code>(a ^ b) =&gt; c</code></p>
  
  <p>Or, what I think  is more correct, will I have to declare, data-types (records, scalars, etc).</p>
  
  <p>From there, the java implementation appears fairly straight-forward from reading the documentation.</p>
  
  <p>It's just the initial translation from inference rules of a type system to propositional logic that is hanging me up.</p>
  
  <p>I think I'm missing some connection between my inference rules (<code>a</code>, and <code>b</code>) and representing them within z3; and as I continue to read the documentation it still remains cloudy as to how to manifest these rules.</p>