As per title:
What is the weakest type of automata that is capable of accepting just the theorems (deducible from any specific set of axioms) of Propositional Calculus (i.e. truth functional logic).
Just to make sure we are all talking about automata types that correspond to types of grammar in Chomsky's hierarchy, I include a link to an depiction of the standard automata - grammar complexity classes:
https://devopedia.org/images/article/210/7090.1571152901.jpg
I believe that the relevant class of automata falls between the classes mentioned in that picture.
First, we must clarify the problem.
In the event that the set of propositional variables is finite, it can be shown that the set of tautologies is context-free. However, the set is clearly not regular, for it if were, then the set of all formulas of the form $P \to [(\neg]^n P )^n$ would also be regular, which it clearly is not.
However, consider the case where the set of propositional variables is infinite. More precisely, let's suppose we have a finite nonempty alphabet $\Sigma$ of variable-name letters, and that a variable name is an element of $\Sigma^+$. Then it can be shown that the language is not context-free. For a proof of all aforementioned facts, see here. The proof of the last fact there is a bit hand-wavy, so I might come back here and flesh it out at some point, but the idea is that if the set of tautologies is context-free, then so too is the set of all propositions of the form $(x_i \to x_j) \to (x_i \to x_j)$, where $x_i$ and $x_j$ are variable names built using a unary encoding of the numbers $i$ and $j$. We can then show that if the aforementioned language is recognised by a nondeterministic pushdown automaton, so too is the set of all strings of the form $a^i b^j c^i d^j$. But this last one is not a context-free language; this can be shown using the pumping theorem for context-free languages.
However, we can decide whether a given propositional formula is a tautology. To do so, we simply iterate through all possible truth assignments and check for each truth assignment that the formula is satisfied. A careful analysis of this algorithm reveals that it can be implemented with a linear-space deterministic Turing machine - that is, it can be accepted by a deterministic bounded linear automaton.
To summarize how this is done, we first write out a candidate truth assignment, which takes linear space. We then copy the original proposition, which again takes linear space. We then substitute the truth assignment into the copy of the original proposition - for instance, if the proposition is $A \lor B$ and the truth assignment is $\{A \mapsto 1, B \mapsto 0\}$, then the copy of the proposition becomes $1 \lor 0$. We then evaluate the truth value of the substituted proposition, which takes constant space. If the truth value is $0$, we halt and determine that our string is not a tautology. If the truth value is $1$, we erase the copy and try to go on to the next truth assignment; if we've run out of truth assignments, we halt and determine that we have a tautology.