I would have guessed that any tautology can be reduced algorithmically to a simpler formula until it becomes p v ~p ??? (So that if the algorithm can't find such a reduction, then that proves it wasn't a tautology.) My main evidence to the contrary is that Rich didn't mention this. —Dan
On Dec 3, 2016, at 6:40 PM, Allan Wechsler <acwacw@gmail.com> wrote:
What does it mean to "solve" a tautology? Is this somehow equivalent to boolean satisfiability?
On Sat, Dec 3, 2016 at 9:36 PM, Henry Baker <hbaker1@pipeline.com> wrote:
At 06:28 AM 12/3/2016, Henry Baker wrote:
1. Is there an easy way to enumerate/generate (all and only) *tautologies* in more-or-less increasing complexity fashion? By complexity, I mean more-or-less increasing fashion wrt the number of distinct variables and the size of the expression.
I thought about this during a long drive today and realized that there *can't* be an "efficient" (P) algorithm to enumerate all and only tautologies, else that algorithm would itself be useful to solve tautologies, and hence P=NP.
So Rich's idea of generating formulae and then doing tautology-testing may well be nearly optimal.