JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants.
Lecture Notes in Computer Science(2001)
摘要
JProver is a first-order intuitionistic theorem prover that creates sequent-style proof objects and can serve as a proof engine in interactive proof assistants with expressive constructive logics. This paper gives a brief overview of JProver’s proof technique, the generation of proof objects, and its integration into the Nuprl proof development system.
更多查看译文
关键词
interactive proof assistants,theorem proving,connection-based
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络