The poor man's proof assistant
Joseph Eremondi · 2013
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.