blob: 2dfb428275fc40d7c4cf4d542a25e786728fced0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
An intuitionistic first-order theorem prover -- JProver.
Usage:
Require 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 JProver.
Coq < Goal (P:Prop) P->P.
1 subgoal
============================
(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.
Structure of this directory:
This directory contains
README ------ this file
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
go ------ batch file to load JProver to Coq dynamically
Comments:
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 formula as
((x:nat) (P x)) -> (EX 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.
|
