While proving a theorem from a set of axioms is undecidable in first order logic, recent development has produced several tools which serve as automated theorem provers. However, often these systems are too complex for a given problem. Their usefulness is outweighed by the difficulty of learning a new tool or translating results into computer-readable form.   I describe tools developed in Prolog to partially characterize the shuffle-inclusion problem. These tools allowed for rapid development of proofs with little intellectual overhead. While focused around a specific problem, the techniques described are general, and well suited to many problems on discrete structures.
['Joey Eremondi']
The poor man's proof assistant: using prolog to develop formal language theoretic proofs