Propositional Logic Random Theorem Generation

[gleachkr]

We'd like to write an module for the generation of random "interesting" theorems, that would serve as effective practice problems.

[JakeEhrlich]

My best idea on how to do this is to randomly generate a sentence (not necessarily a valid one), test it for validity (which with a small number of variables, say 3, would be easy). If it is valid then return the sentence; if it is not valid then return the negation of the sentence. We can then randomly push negations in or out, change operators from one form to another, etc... Also I think the initial step will produce a small fraction of un-negated sentences. To combat this we can simply sample multiple times from this process and choose the un-negated one if it exists.

Does this sound like a good implementation?

[gleachkr]

I think it might be a little harder than that. There are two issues that I think we might want to tackle separately. One is just generating random valid sentences. I think something like what you're describing, maybe with some additional validity checks (we might not get a valid sentence by negating an invalid one) might work for that. The other is ensuring that the proofs are "interesting".

That's a little bit harder to specify as a goal. It might be easier to give some "boring-making" features, and try to filter those out. For example, you might think that a disjunction, which has a valid disjunct, would not be interesting to prove, since a big part of the formula will turn out to be irrelevant to the proof. the interesting cases would be when the validity comes from interaction between the disjuncts. Similarly for other connectives, perhaps.