Character and Operation Rule of the Classifier in First Logic Reasoning System F
Meng Ling-jiang · Journal of Hebei University · 2008
The classifier is playing the vital role in first logic reasoning.However its poeration rule is more comples.Some of equivalent types and the implication type can't be proved by the matrix unlike propositional logic.This article will summarize them and give a series of proofs.