Nested Proof Compilation and Proof Checking in Universal Pattern Logic

摘要

In this paper, we discuss the connections between proofs in logics with axiomatic deduction system and the deduction problems of a logic called first order universal pattern logic (UPL-1). We propose a method which can efficiently convert proofs in axiomatic logics to formula sequences in UPL-1 whereby we can check the validity of the proofs, and then a decidable proof checking approach is sketched out.