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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
open Dpctypes;;
open Kwc;;
open Lk_proofs;;
exception Not_provable_in_DPC of string
;;
exception No_intuitionnistic_proof of int
;;
(* is_int_proof : lkproof2 -> bool *******)
let rec is_int_proof (Proof2(sq1,sq2,rule)) =
if (List.length sq2)>1 then false
else match rule with
Axiom2(_) -> true
| RWeakening2(_,p) -> is_int_proof p
| LWeakening2(_,p) -> is_int_proof p
| RNeg2(_,p) -> is_int_proof p
| LNeg2(_,p) -> is_int_proof p
| RConj2(_,p1,_,p2) -> (is_int_proof p1) & (is_int_proof p2)
| LConj2(_,_,p) -> is_int_proof p
| RDisj2(f1,f2,Proof2(_,_,RWeakening2(f3,p))) ->
if (f3=f1) or (f3=f2) then is_int_proof p
else false
| RDisj2(_,_,_) -> false
| LDisj2(_,p1,_,p2) -> (is_int_proof p1) & (is_int_proof p2)
| RImp2(_,_,p) -> is_int_proof p
| LImp2(_,p1,_,p2) -> (is_int_proof p1) & (is_int_proof p2)
| RForAll2(_,_,p) -> is_int_proof p
| LForAll2(_,_,_,p) -> is_int_proof p
| RExists2(_,_,_,p) -> is_int_proof p
| LExists2(_,_,p) -> is_int_proof p
;;
(* find_int_proof : f -> f1 -> path list -> lkproof2 *****)
let find_int_proof f f1 all_v_paths =
let rec find_rec = function
p::ll -> let pr0 = proof_of_path [Po(f1)] p in
if is_int_proof pr0
then int_quant f (snd p) pr0
else find_rec ll
| [] -> raise Not_found
in find_rec all_v_paths
;;
(* prove_f : formula -> lk_proof2
prove : string -> lk_proof2 *******)
let prove_f f =
let f0 = separate f
in let (ex,f1) = herbrand f0
in let (pos,neg,lcj) = lit_conj f1
in let cj = List.map (fun (c,_) -> c) lcj
in let m = all_matches pos neg lcj
in if m = []
then raise (Not_provable_in_DPC "(No match)")
else let all_paths = paths pos neg m lcj
in if all_paths = []
then raise (Not_provable_in_DPC "(No path)")
else let all_valid_paths = good_paths lcj all_paths
in if all_valid_paths = []
then raise (Not_provable_in_DPC "(No valid path)")
else try find_int_proof f f1 all_valid_paths
with Not_found -> let n = List.length all_valid_paths
in raise (No_intuitionnistic_proof n)
;;
|
