Journal of automated reasoning. 1997;18(1):105-134. doi: 10.1023/a:1005749401809 Q40.72025
Unification Algorithms for Eliminating and Introducing Quantifiers in Natural Deduction Automated Theorem Proving
自然演绎自动定理证明中消除与引入量词的统一算法
DOI: 10.1023/a:1005749401809
摘要 查看摘要
