package coq-jprover
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
A theorem prover for first-order intuitionistic logic
Install
Dune Dependency
Authors
Maintainers
Sources
v8.5.0.tar.gz
md5=219a58c98b9a61b99c625d8c6d5b69ff
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:April 2002 (contribution since January 2009)Published: 07 Jun 2016
On This Page