package coq-jprover

  1. Overview
  2. No Docs
A theorem prover for first-order intuitionistic logic

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. H
    Huang Guan-Shieng

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

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

Dependencies (2)

  1. coq >= "8.6" & < "8.7~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None