package coq-jprover
A theorem prover for first-order intuitionistic logic
Install
Dune Dependency
Authors
Maintainers
Sources
v8.6.0.tar.gz
md5=d7a8888e2da482827e2bc958d6902b89
Description
JProver is a theorem prover for first-order intuitionistic logic. It is originally implemented by Stephan Schmitt and then integrated into MetaPRL by Aleksey Nogin. After this, Huang Guan-Shieng extracted the necessary ML-codes from MetaPRL and then adapted it to Coq.
Tags
keyword: decision procedure keyword: first-order logic keyword: intuitionistic logic keyword: theorem proving keyword: proof search category: Miscellaneous/Coq Extensions category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures date: 2002-04 (contribution since January 2009)Published: 20 Nov 2018
On This Page