I’m currently implementing a system for guiding automated inductive proof for my dissertation. Whereas normally these systems work over functional expressions, mine works on relational expressions (“relational rippling”).
My current corpus that I’m using to test the system consists of functional theorems translated into a relational form, i.e. simple Prolog predicates. It’s been brought to my attention that there’s a worry that these are too specific, too functional, and I should expand the corpus in new directions. Two directions were suggested to me - operational semantics of programming languages and electronic circuits (as relational expressions are often used for proving circuit correctness, anyway - predicates are used for logic gates and shared existential variables for wires between them).
The operational semantics I’ve got covered.
Unfortunately, there’s a few problems with the circuits. Our AI library was destroyed a few years ago in a fire, so all the books and papers that I need were incinerated. I’ve been trying to find some logic circuits that are simple enough (I’ve found plenty by Gordon et al, for example, who verified a whole computer, but these are too complicated), amenable to induction (they need to have some sort of time component or some other property that allows them to be reasoned about by induction) but not overly simple (my limited electronics knowledge only allows me to come up with very simple, boring examples). The circuits also need a specification, too. I can’t prove anything about them if I don’t understand what they’re supposed to do!
So, electronic engineers, do you know of any course notes or relevant papers that are likely to have some examples? If the circuits are actually useful for something (i.e. not just made up on the spot, but used in real world appliances), then this would be even better (but I’m not fussy!).
Thanks for your help.