summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/FOL/intprover.ML

changeset 2601 | b301958c465d |

parent 2572 | 8a47f85e7a03 |

child 4440 | 9ed4098074bc |

equal
deleted
inserted
replaced

2600:be48eff459e9 | 2601:b301958c465d |
---|---|

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 Intuitionistic Logic. |

27 val step_tac: int -> tactic |
27 val step_tac: int -> tactic |

28 val haz_brls: (bool * thm) list |
28 val haz_brls: (bool * thm) list |

29 end; |
29 end; |

30 |
30 |

31 |
31 |

32 structure Int : INT_PROVER = |
32 structure IntPr : INT_PROVER = |

33 struct |
33 struct |

34 |
34 |

35 (*Negation is treated as a primitive symbol, with rules notI (introduction), |
35 (*Negation is treated as a primitive symbol, with rules notI (introduction), |

36 not_to_imp (converts the assumption ~P to P-->False), and not_impE |
36 not_to_imp (converts the assumption ~P to P-->False), and not_impE |

37 (handles double negations). Could instead rewrite by not_def as the first |
37 (handles double negations). Could instead rewrite by not_def as the first |