  Despite recent advances in automating theorem proving in full first-order
theories, inductive reasoning still poses a serious challenge to
state-of-the-art theorem provers. The reason for that is that in first-order
logic induction requires an infinite number of axioms, which is not a feasible
input to a computer-aided theorem prover requiring a finite input. Mathematical
practice is to specify these infinite sets of axioms as axiom schemes.
Unfortunately these schematic definitions cannot be formalized in first-order
logic, and therefore not supported as inputs for first-order theorem provers.
  In this work we introduce a new method, inspired by the field of axiomatic
theories of truth, that allows to express schematic inductive definitions, in
the standard syntax of multi-sorted first-order logic. Further we test the
practical feasibility of the method with state-of-the-art theorem provers,
comparing it to solvers' native techniques for handling induction.
  This paper is an extended version of the LFMTP 21 submission with the same
title.
