ABSFOL: A Proof Checker with Abstraction

摘要

Let SIGMA_i= be a formal system, where LAMBDA_i is a first order language, OMEGA_i a set of axioms, and DELTA_i a set of inference rules. An abstraction is a pair of formal systems SIGMA_g and SIGMA_a, together with a total function f_LAMBDA:LAMBDA_g=>LAMBDA_a. From now on we use the word "context" as a synonym of "formal system". We also use the terms "ground" and "abstract" to denote (bojects of) SIGMA_g and SIGMA_a respectively (e.g. the "ground language" is the language of SIGMA_g).