# Contribution: JProver

A theorem prover for first-order intuitionistic logic

## Authors

• Huang Guan-Shieng

## 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.

## Keywords

decision procedures, first order logic, intuitionistic logic, theorem proving, proof search

```An intuitionistic first-order theorem prover -- JProver.

Usage:

Require Import JProver.
jp [num].

Whem [num] is provided, proof is done automatically with
the multiplicity limit [num], otherwise no limit is forced
and JProver may not terminate.

Example:

Require Import JProver.
Coq < Goal forall P:Prop, P->P.
1 subgoal

============================
forall P:Prop, P->P

Unnamed_thm < jp 1.
Proof is built.
Subtree proved!
-----------------------------------------

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 (see jall.ml). After this, Huang extracted the
necessary ML-codes from MetaPRL and then integrated it into Coq.
integrating JProver into interactive proof assistants, please refer to

"Stephan Schmitt, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin,
Jprover: Integrating connection-based theorem proving into interactive
proof assistants. In International Joint Conference on Automated
Reasoning, volume 2083 of Lecture Notes in Artificial Intelligence,
pages 421-426. Springer-Verlag, 2001" -
http://www.cs.cornell.edu/nogin/papers/jprover.html

Structure of this directory:
This directory contains

jall.ml         ------  the main module of JProver
jtunify.ml      ------  string unification procedures for jall.ml
jlogic.ml       ------  interface module of jall.ml
jterm.ml
opname.ml       ------  implement the infrastructure for jall.ml
jprover.ml      ------  the interface of jall.ml to Coq
JProver.v       ------  declaration for Coq
Makefile        ------  the makefile

1. The original <jall.ml> is located in meta-prl/refiner/reflib of the
MetaPRL directory. Some parts of this file are modified by Huang.

2. <jtunify.ml> is also located in meta-prl/refiner/reflib with no modification.

3. <jlogic.ml> is modified from meta-prl/refiner/reflib/jlogic_sig.mlz.

4. <jterm.ml> and <opname.ml> are modified from the standard term module
of MetaPRL in meta-prl/refiner/term_std.

5. The jp tactic currently cannot prove formulas such as
(forall x:nat, P x) -> (exists y:nat, P y), which requires extra constants
in the domain when the left-All rule is applied.

by Huang Guan-Shieng (Guan-Shieng.Huang@lri.fr), March 2002.

```