%I #46 Jul 02 2020 09:19:30
%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 non-ASCII characters).
%C Formally, the language used for this sequence contains the symbols a-z and A-Z (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