equal
deleted
inserted
replaced
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 A naive prover for intuitionistic logic |
6 A naive prover for intuitionistic logic |
7 |
7 |
8 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ... |
8 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ... |
9 |
9 |
10 Completeness (for propositional logic) is proved in |
10 Completeness (for propositional logic) is proved in |
11 |
11 |
12 Roy Dyckhoff. |
12 Roy Dyckhoff. |
13 Contraction-Free Sequent Calculi for Intuitionistic Logic. |
13 Contraction-Free Sequent Calculi for IntPruitionistic Logic. |
14 J. Symbolic Logic (in press) |
14 J. Symbolic Logic (in press) |
15 *) |
15 *) |
16 |
16 |
17 signature INT_PROVER = |
17 signature INT_PROVER = |
18 sig |
18 sig |
25 val step_tac: int -> tactic |
25 val step_tac: int -> tactic |
26 val haz_brls: (bool * thm) list |
26 val haz_brls: (bool * thm) list |
27 end; |
27 end; |
28 |
28 |
29 |
29 |
30 structure Int : INT_PROVER = |
30 structure IntPr : INT_PROVER = |
31 struct |
31 struct |
32 |
32 |
33 (*Negation is treated as a primitive symbol, with rules notI (introduction), |
33 (*Negation is treated as a primitive symbol, with rules notI (introduction), |
34 not_to_imp (converts the assumption ~P to P-->False), and not_impE |
34 not_to_imp (converts the assumption ~P to P-->False), and not_impE |
35 (handles double negations). Could instead rewrite by not_def as the first |
35 (handles double negations). Could instead rewrite by not_def as the first |