Representing inference rules in z3

Question

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.

Let's say I have the following 2 inference rules:

Is it so simple that my z3 rules will be:

a. (a ^ b) => c
b. (a ^ b) => c

Or, what I think is more correct, will I have to declare, data-types (records, scalars, etc).

From there, the java implementation appears fairly straight-forward from reading the documentation.

It's just the initial translation from inference rules of a type system to propositional logic that is hanging me up.

I think I'm missing some connection between my inference rules (a, and b) and representing them within z3; and as I continue to read the documentation it still remains cloudy as to how to manifest these rules.

Answer 1

Z3 would be a fine choice for this task, though it is really hard to follow exactly what your question is. (The bullet points a and b you have are exactly the same, was that intentional?) But essentially inference rules are implications, so thinking about them in terms of propositions and implications between them would be just fine.

Furthermore, your rules probably will have a Horn structure them (as in Horn clauses as found in Prolog, see here: https://en.wikipedia.org/wiki/Horn_clause), and Z3 has a datalog engine that can make coding such problems even easier.

See here for a very nice introduction: http://rise4fun.com/z3/tutorialcontent/fixedpoints which I think can be adopted to your use case with relative ease.