2 ID: $Id$ |
2 ID: $Id$ |
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 Generic tableau prover with proof reconstruction |
6 Generic tableau prover with proof reconstruction |
|
7 |
|
8 Why does Abs take a string argument? |
7 |
9 |
8 SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules?? |
10 SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules?? |
9 Needs explicit instantiation of assumptions? |
11 Needs explicit instantiation of assumptions? |
10 |
12 |
11 |
13 |
18 * rules must not require higher-order unification, e.g. apply_type in ZF |
20 * rules must not require higher-order unification, e.g. apply_type in ZF |
19 + message "Function Var's argument not a bound variable" relates to this |
21 + message "Function Var's argument not a bound variable" relates to this |
20 * its proof strategy is more general but can actually be slower |
22 * its proof strategy is more general but can actually be slower |
21 |
23 |
22 Known problems: |
24 Known problems: |
|
25 With overloading: |
|
26 1. Overloading can't follow all chains of type dependencies. Cannot |
|
27 prove "In1 x ~: Part A In0" because PartE introducees the polymorphic |
|
28 equality In1 x = In0 y, when the corresponding rule uses the (distinct) |
|
29 set equality. Workaround: supply a type instance of the rule that |
|
30 creates new equalities (e.g. PartE in HOL/ex/Simult) |
|
31 ==> affects freeness reasoning about Sexp constants (since they have |
|
32 type ... set) |
|
33 |
23 With substition for equalities (hyp_subst_tac): |
34 With substition for equalities (hyp_subst_tac): |
24 1. Sometimes hyp_subst_tac will fail due to occurrence of the parameter |
35 1. Sometimes hyp_subst_tac will fail due to occurrence of the parameter |
25 as the argument of a function variable |
36 as the argument of a function variable |
26 2. When substitution affects a haz formula or literal, it is moved |
37 2. When substitution affects a haz formula or literal, it is moved |
27 back to the list of safe formulae. |
38 back to the list of safe formulae. |
295 in subst (t,0) end; |
306 in subst (t,0) end; |
296 |
307 |
297 |
308 |
298 (*Normalize...but not the bodies of ABSTRACTIONS*) |
309 (*Normalize...but not the bodies of ABSTRACTIONS*) |
299 fun norm t = case t of |
310 fun norm t = case t of |
300 Skolem(a,args) => Skolem(a, vars_in_vars args) |
311 Skolem (a,args) => Skolem(a, vars_in_vars args) |
301 | (Var (ref None)) => t |
312 | (Var (ref None)) => t |
302 | (Var (ref (Some u))) => norm u |
313 | (Var (ref (Some u))) => norm u |
303 | (f $ u) => (case norm f of |
314 | (f $ u) => (case norm f of |
304 Abs(_,body) => norm (subst_bound (u, body)) |
315 Abs(_,body) => norm (subst_bound (u, body)) |
305 | nf => nf $ norm u) |
316 | nf => nf $ norm u) |
312 Some u => wkNorm u |
323 Some u => wkNorm u |
313 | None => t) |
324 | None => t) |
314 | (f $ u) => (case wkNormAux f of |
325 | (f $ u) => (case wkNormAux f of |
315 Abs(_,body) => wkNorm (subst_bound (u, body)) |
326 Abs(_,body) => wkNorm (subst_bound (u, body)) |
316 | nf => nf $ u) |
327 | nf => nf $ u) |
|
328 | Abs (a,body) => (*eta-contract if possible*) |
|
329 (case wkNormAux body of |
|
330 nb as (f $ t) => |
|
331 if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0 |
|
332 then Abs(a,nb) |
|
333 else wkNorm (incr_boundvars ~1 f) |
|
334 | nb => Abs (a,nb)) |
317 | _ => t |
335 | _ => t |
318 and wkNorm t = case head_of t of |
336 and wkNorm t = case head_of t of |
319 Const _ => t |
337 Const _ => t |
320 | OConst _ => t |
338 | OConst _ => t |
321 | Skolem(a,args) => t |
339 | Skolem(a,args) => t |
628 in |
646 in |
629 fun normBr (br, lits, vars, lim) = |
647 fun normBr (br, lits, vars, lim) = |
630 (map normLev br, map norm lits, vars, lim); |
648 (map normLev br, map norm lits, vars, lim); |
631 |
649 |
632 fun tracing brs = if !trace then fullTrace := map normBr brs :: !fullTrace |
650 fun tracing brs = if !trace then fullTrace := map normBr brs :: !fullTrace |
633 else () |
651 else () |
634 end; |
652 end; |
635 |
653 |
636 |
654 |
637 exception PROVE; |
655 exception PROVE; |
638 |
656 |
738 Const "*Goal*" $ G :: (if exists bad lits then change lits else lits) |
756 Const "*Goal*" $ G :: (if exists bad lits then change lits else lits) |
739 end |
757 end |
740 | addLit (G,lits) = ins_term(G, lits) |
758 | addLit (G,lits) = ins_term(G, lits) |
741 |
759 |
742 |
760 |
743 (*For calculating the "penalty" to assess on a branching factor of n*) |
761 (*For calculating the "penalty" to assess on a branching factor of n |
744 fun log2 1 = 0 |
762 log2 seems a little too severe*) |
745 | log2 n = 1 + log2(n div 2); |
763 fun log3 n = if n<3 then 0 else 1 + log3(n div 3); |
746 |
764 |
747 |
765 |
748 (*Tableau prover based on leanTaP. Argument is a list of branches. Each |
766 (*Tableau prover based on leanTaP. Argument is a list of branches. Each |
749 branch contains a list of unexpanded formulae, a list of literals, and a |
767 branch contains a list of unexpanded formulae, a list of literals, and a |
750 bound on unsafe expansions.*) |
768 bound on unsafe expansions.*) |
779 | deeper (((P,prems),tac)::grls) = |
797 | deeper (((P,prems),tac)::grls) = |
780 let val dummy = unify(add_term_vars(P,[]), P, G) |
798 let val dummy = unify(add_term_vars(P,[]), P, G) |
781 (*P comes from the rule; G comes from the branch.*) |
799 (*P comes from the rule; G comes from the branch.*) |
782 val ntrl' = !ntrail |
800 val ntrl' = !ntrail |
783 val lim' = if ntrl < !ntrail |
801 val lim' = if ntrl < !ntrail |
784 then lim - (1+log2(length rules)) |
802 then lim - (1+log3(length rules)) |
785 else lim (*discourage branching updates*) |
803 else lim (*discourage branching updates*) |
786 val vars = vars_in_vars vars |
804 val vars = vars_in_vars vars |
787 val vars' = foldr add_terms_vars (prems, vars) |
805 val vars' = foldr add_terms_vars (prems, vars) |
788 val choices' = (ntrl, nbrs, PRV) :: choices |
806 val choices' = (ntrl, nbrs, PRV) :: choices |
789 val tacs' = (DETERM o (tac false)) :: tacs |
807 val tacs' = (DETERM o (tac false)) :: tacs |
877 val vars = vars_in_vars vars |
895 val vars = vars_in_vars vars |
878 val vars' = foldr add_terms_vars (prems, vars) |
896 val vars' = foldr add_terms_vars (prems, vars) |
879 val dup = md andalso vars' <> vars |
897 val dup = md andalso vars' <> vars |
880 (*duplicate H only if md and the premise has new vars*) |
898 (*duplicate H only if md and the premise has new vars*) |
881 val lim' = (*Decrement "lim" extra if updates occur*) |
899 val lim' = (*Decrement "lim" extra if updates occur*) |
882 if ntrl < !ntrail then lim - (1+log2(length rules)) |
900 if ntrl < !ntrail then lim - (1+log3(length rules)) |
883 else lim-1 |
901 else lim-1 |
884 (*NB: if the formula is duplicated, |
902 (*NB: if the formula is duplicated, |
885 then it seems plausible to leave lim alone. |
903 then it seems plausible to leave lim alone. |
886 But then transitivity laws loop.*) |
904 But then transitivity laws loop.*) |
887 val mayUndo = not (null grls) (*other rules to try?*) |
905 val mayUndo = not (null grls) (*other rules to try?*) |