如何在自然演绎中证明：一种策略方法
计算机与社会
2015-07-15 v1 计算机科学中的逻辑
摘要
本文的动机源于我们教授自然演绎（ND）的经验，以及这一形式系统在 \textsc{Coq} 证明助手中的实现方式，即通过所谓的策略，这些策略是将目标公式转化为一系列子目标的启发式方法，而这些子目标的可证性蕴含原公式的可证性。我们旨在将其中一些策略引入极小逻辑的 ND 系统中。我们的目标有两个：形式化与教学。前者提供了一个形式系统及其构建证明的底层启发式方法，这反过来又服务于我们的后一个目的，即为计算机科学专业本科阶段的 ND 教学构建一个理想的系统。
引用
@article{arxiv.1507.03678,
title = {How to prove it in Natural Deduction: A Tactical Approach},
author = {Favio E. Miranda-Perea and P. Selene Linares-Arévalo and Atocha Aliseda},
journal= {arXiv preprint arXiv:1507.03678},
year = {2015}
}
备注
Proceedings of the Fourth International Conference on Tools for Teaching Logic (TTL2015), Rennes, France, June 9-12, 2015. Editors: M. Antonia Huertas, Jo\~ao Marcos, Mar\'ia Manzano, Sophie Pinchinat, Fran\c{c}ois Schwarzentruber