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 (<->).
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).
Formally, the language used for this sequence contains the symbols a-z and A-Z (the variables),~,*,+,->,<->,( and ).
The formulas are defined by the following rules:
* Every variable is a formula.
* If A is a formula, then ~A is a formula.
* If A and B are formulas, then (A*B), (A+B), (A->B) and (A<->B) are all formulas.
A formula is a tautology if it is true for any assignment of truth values to the variables.
