There's another way to check tautologies: Pick a variable, and substitute T for it. Then do the same thing, but substitute F. If both formulas are already in your list, then you have a new theorem. This can be run backwards as a non-shrink taut-gen algorithm: Use Clark's operators as a base, and generate all {T,F}-only formulas, sorting them into either the evaluates-to-T list or the evaluates-to-F list. Start each list with the formula T, or F. Grow new formulas by substituting any single instance of T with one of T&T, TvT, TvF, FvT, ~F, T->T, etc., or subbing an F with ~T, T&F, etc. To introduce variables, find pairs of True formulas whose operator structure & grouping match. Line up the formulas to match individual letters (T, F, or a prior variable). Any existing variables must also match. Variables don't match Ts or Fs. All T/F mismatches are replaced with the new variable V, and all F/T mismatches with ~V. The result goes into a True-formulas-with-variables list; whenever all the Ts and Fs are gone, we have a theorem. So we might have the True propositions T->T and F->F, and combine them to get P->P. We could build up P->(PvQ) in steps, from the intermediates P->(PvT) and P->(PvF). This could hardly be called efficient, but it is non-shrink. Rich ________________________________________ From: math-fun [math-fun-bounces@mailman.xmission.com] on behalf of W. Edwin Clark [wclark@mail.usf.edu] Sent: Saturday, December 3, 2016 2:31 PM To: math-fun Subject: [EXTERNAL] Re: [math-fun] propositional logic tautologies http://oeis.org/A256120 a(n) is the number of tautologies that are n symbols long in propositional calculus with the connectives not (~), and (*), or (+), implies (->) and if and only if (<->). On Sat, Dec 3, 2016 at 9:28 AM, Henry Baker <hbaker1@pipeline.com> wrote:
I'm a little rusty on my propositional logic, so I can't remember (if I ever knew) the answer to the following questions:
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.
2. What % of prop logic expressions (of a particular complexity) are tautologies?
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun