  There is an increasing interest in applying recent advances in AI to
automated reasoning, as it may provide useful heuristics in reasoning over
formalisms in first-order, second-order, or even meta-logics. To facilitate
this research, we present MATR, a new framework for automated theorem proving
explicitly designed to easily adapt to unusual logics or integrate new
reasoning processes. MATR is formalism-agnostic, highly modular, and
programmer-friendly. We explain the high-level design of MATR as well as some
details of its implementation. To demonstrate MATR's utility, we then describe
a formalized metalogic suitable for proofs of G\"odel's Incompleteness
Theorems, and report on our progress using our metalogic in MATR to
semi-autonomously generate proofs of both the First and Second Incompleteness
Theorems.
