Computational Reflection via Mechanized Logical Deduction