%I
%S 0,0,0,0,2,2,12,6,57,88,373,554,2198,5413,20397
%N Number of tautologies in propositional calculus of length n.
%C 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 (<>).
%C When measuring the length of a tautology, all brackets must be included. The connectives > and <> are counted as one symbol each (but writing them as such requires nonASCII characters).
%C Formally, the language used for this sequence contains the symbols az and AZ (the variables),~,*,+,>,<>,( and ).
%C The formulas are defined by the following rules:
%C * Every variable is a formula.
%C * If A is a formula, then ~A is a formula.
%C * If A and B are formulas, then (A*B), (A+B), (A>B) and (A<>B) are all formulas.
%C A formula is a tautology if it is true for any assignment of truth values to the variables.
%H Matthew Scroggs, <a href="http://www.mscroggs.co.uk/blog/16">Logic Bot, pt. 2</a>
%H Matthew Scroggs, <a href="http://www.mscroggs.co.uk/blog/tautologies.txt">List of tautologies</a>
%e The tautologies of length 5 are (a>a) and (a<>a).
%e The tautologies of length 6 are (~a+a) and (a+~a).
%e The tautologies of length 7 are (~~a>a), (~~a<>a), (~a>~a), (~a<>~a), (a>~~a), (a<>~~a), ~(~a<>a), ~(~a*a), ~(a<>~a), ~(a*~a), ~~(a>a) and ~~(a<>a).
%Y Cf. A277275, A277276
%K nonn,more
%O 1,5
%A _Matthew Scroggs_, Mar 15 2015
%E More terms from _Matthew Scroggs_, Mar 27 2015
%E Typo in a(11) corrected by _Matthew Scroggs_, Mar 27 2015
%E a(13) corrected, and a(14)a(15) added by _Matthew Scroggs_, Jul 02 2020
