30 Have of rich_sequent | |
30 Have of rich_sequent | |
31 Cases of (clause * direct_inference list) list |
31 Cases of (clause * direct_inference list) list |
32 |
32 |
33 type direct_proof = direct_inference list |
33 type direct_proof = direct_inference list |
34 |
34 |
35 val make_refute_graph : (atom list * atom) list -> refute_graph |
35 val make_refute_graph : atom -> (atom list * atom) list -> refute_graph |
36 val axioms_of_refute_graph : refute_graph -> atom list -> atom list |
36 val axioms_of_refute_graph : refute_graph -> atom list -> atom list |
37 val tainted_atoms_of_refute_graph : refute_graph -> atom list -> atom list |
37 val tainted_atoms_of_refute_graph : refute_graph -> atom list -> atom list |
38 val sequents_of_refute_graph : refute_graph -> ref_sequent list |
38 val sequents_of_refute_graph : refute_graph -> ref_sequent list |
39 val string_of_refute_graph : refute_graph -> string |
39 val string_of_refute_graph : refute_graph -> string |
40 val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent |
40 val redirect_sequent : atom list -> atom -> ref_sequent -> direct_sequent |
70 fun atom_eq p = (Atom.ord p = EQUAL) |
70 fun atom_eq p = (Atom.ord p = EQUAL) |
71 fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d)) |
71 fun clause_eq (c, d) = (length c = length d andalso forall atom_eq (c ~~ d)) |
72 fun direct_sequent_eq ((gamma, c), (delta, d)) = |
72 fun direct_sequent_eq ((gamma, c), (delta, d)) = |
73 clause_eq (gamma, delta) andalso clause_eq (c, d) |
73 clause_eq (gamma, delta) andalso clause_eq (c, d) |
74 |
74 |
75 fun make_refute_graph infers = |
75 fun make_refute_graph bot infers = |
76 let |
76 let |
77 fun add_edge to from = |
77 fun add_edge to from = |
78 Atom_Graph.default_node (from, ()) |
78 Atom_Graph.default_node (from, ()) |
79 #> Atom_Graph.default_node (to, ()) |
79 #> Atom_Graph.default_node (to, ()) |
80 #> Atom_Graph.add_edge_acyclic (from, to) |
80 #> Atom_Graph.add_edge_acyclic (from, to) |
81 fun add_infer (froms, to) = fold (add_edge to) froms |
81 fun add_infer (froms, to) = fold (add_edge to) froms |
82 in Atom_Graph.empty |> fold add_infer infers end |
82 val graph = fold add_infer infers Atom_Graph.empty |
|
83 val reachable = Atom_Graph.all_preds graph [bot] |
|
84 in graph |> Atom_Graph.restrict (member (is_equal o Atom.ord) reachable) end |
83 |
85 |
84 fun axioms_of_refute_graph refute_graph conjs = |
86 fun axioms_of_refute_graph refute_graph conjs = |
85 subtract atom_eq conjs (Atom_Graph.minimals refute_graph) |
87 subtract atom_eq conjs (Atom_Graph.minimals refute_graph) |
86 |
88 |
87 fun tainted_atoms_of_refute_graph refute_graph = |
89 fun tainted_atoms_of_refute_graph refute_graph = |