This goes very deep actually. Strange that Wikipedia never mentions it.
What you are looking for are very hard proofs that can, probably, be reached with things like Fitch proofs. So we are trying to deduct things out of our given data. There are a lot of Fitch proof builders that do a lot of work for you. But some exercises are just not to proof.
I don't know if the user should do the calculations. If so, be aware of things like 3SAT, which are undoable problems for polynomial time.
As for the data structures you want to use, I think you want to have some kind of
Rule class. The rule can be anything, depending on the type. There aren't a lot of rules in predicate logics, so this can be overcome by inheriting (if, iff, and, or, not...). These rules only have to be evaluated. And the only thing a rule can do, is return true or false. Because that is what you do with predicate logics. At university, I was recommended to read this book by John Kelly.
Going back to the classes: You should see these problems like you would see implementing normal calculations with math. What is a
+ operator? It contains two parameters, which can be a new equation by itself, or just a number. I think you have the same with Rules. They can have new Rules as a parameter, or just a boolean (so called predicate).
I hope this helps you a lot, especially the references. If you want to know more, or if I'm going into the wrong direction, please tell me.