Creating artificial NP-Complete problems
Dodging any questions about whether this is "interesting" or "artificial" (or whether Computer Science really needs any more NP-complete problems than it already has), the answer is "yes".  Pick a structure-preserving mapping between some set of strings and problem instances of 3SAT.  Show that the mapping can be computed in polynomial time (i.e., it is a polytime reduction).  Then, deciding if a string is in your set of strings is NP-complete.  Repeat as desired (the composition of polytime reductions is a polytime reduction.)

If you wanted to automate this process of creating new NP-complete problems, then it would likely be more efficient to construct the mappings from some base set of polytime mappings, using methods known to preserve polynomial time, rather than picking an arbitrary mapping and proving that it is a polytime reduction.

Note that this is not quite what you suggest in your question.  You can take a logical formula and build a Turing machine corresponding to it, but that in itself doesn't lead to an NP-complete problem.  For instance, 2SAT instances can be decided in polynomial time.  And a particular formula will only correspond to a particular machine, whereas you need a set of formulas (or machines) to define a complexity class; so to make new problems in NPC, you really need to show how one set can be converted into another (i.e. a polytime reduction), even if your sets are sets of logical formulas.