Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo

Guillaume Burel

In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for…