Post canonical system
A Post canonical system is a formalism for modelling logical theories, developed by Emil Post in the 1930's.
A Post canonical system contains a set called axioms, which are strings over a given alphabet of symbols. It also contains a set of productions, each of which contains a antecedent and a consequent. Each of these is what we would think of as "patterns" nowadays - a string of symbols from the alphabet, which may also contain "wildcards". Each "wildcard" in the antecedent can match any number of symbols; the corresponding "wildcard" in the consequent is substituted with the thing that was matched.
To prove a conjecture within a Post canonical system, one starts with one of the axioms and attempts to derive the conjecture by repeatedly applying the productions to it. In this way, a Post canonical system describes a formal language - the set of conjectures (strings) which the system can prove (generate).
For example, take the following axiom:
and the following productions:
1. n → (n) 2. n → n()
and say we want to prove or disprove the conjecture
We can start with the axiom
apply production 2 to yield
and then apply production 1 to yield
thus proving the conjecture.
Post canonical systems have been shown to be in the same computational class as Turing machines, that is, they are Turing-complete. They can be seen as (probably) the first approach to string-rewriting.
Post canonical systems can have further restrictions imposed upon them and still be Turing-complete. Post normal systems, for example, can only have one "wildcard" in each production - at the end of the antecedent and the beginning of the consequent. Tag systems are even more restricted than that.