Abduction: decremental conjecture identification in each layer. about psl HOT 19 OPEN

We can inspect the proof scripts suggested by Sledgehammer to identify useful conjectures.

from psl.

I have to work on not only the production of conjectures in work_on_ornode in Proof_By_Abduction.ML but also add_or2and_edge in Seed_Of_And_Node.ML.

One critical question is what conjectures we should store in the and-node? All-conjectures? Conjectures whose names appear in the SH output?

We should opt for a solution that is consistent with other cases.

from psl.

In the current implementation, we
-1. add and-nodes in https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Proof_By_Abduction.ML#LL43C37-L43C50

• 2a. add child-ornodes in

  PSL/Abduction/Proof_By_Abduction.ML

  Line 44 in 9084e8e

  val graph_w_ornodes(*expensive*) = fold (add_child_ornodes_for_this_andnode pst) new_andnds_keys graph_w_andnodes : abduction_graph;

• 2b This function also adds edges from the and-node to its child-or-nodes.

  PSL/Abduction/Update_Abduction_Graph.ML

  Line 220 in 9084e8e

  val graph_w_edges = add_edges_from_andnodes_to_ornodes [and_key] graph_w_ornodes: abduction_graph;

• 3a. add or-to-and edges in

  PSL/Abduction/Proof_By_Abduction.ML

  Line 47 in 9084e8e

  val graph_w_ornodes_n_or2add_edges = fold (SOAN.add_or2and_edge or_key) seeds_of_newly_added_andnodes graph_w_ornodes: abduction_graph;

  
  

  PSL/Abduction/Seed_Of_And_Node.ML

  Line 151 in 9084e8e

  |> PGraph.new_node (or2and_edge_key, or2and_edge_val)

• 3b. This function also connects the parental or-node to the labelled edge.
  

  PSL/Abduction/Seed_Of_And_Node.ML

  Line 152 in 9084e8e

  |> Update_Abduction_Graph.add_edge_acyclic_if_possible or_key or2and_edge_key

• 3c. This function also connects the labelled edge to the and-node.
  

  PSL/Abduction/Seed_Of_And_Node.ML

  Line 152 in 9084e8e

  |> Update_Abduction_Graph.add_edge_acyclic_if_possible or_key or2and_edge_key

• 3d. cut edges to and-nodes inside add_or2and_edge in Seed_Of_And_Node.ML

  PSL/Abduction/Seed_Of_And_Node.ML

  Line 155 in 9084e8e

  val result = cut_edge_to_andnode_if_no_parental_ornode_can_be_proved_assmng_subgoals andnode_key or2and_edge_key graph_w_or2and_edge_connected;

Should we also cut edges to the or-nodes that represent conjectures that are not used in SH's output?

from psl.

In the current implementation, we -1. add and-nodes in https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Proof_By_Abduction.ML#LL43C37-L43C50

• 2a. add child-ornodes in

  PSL/Abduction/Proof_By_Abduction.ML

  Line 44 in 9084e8e

  val graph_w_ornodes(*expensive*) = fold (add_child_ornodes_for_this_andnode pst) new_andnds_keys graph_w_andnodes : abduction_graph;

• 2b This function also adds edges from the and-node to its child-or-nodes.

  PSL/Abduction/Update_Abduction_Graph.ML

  Line 220 in 9084e8e

  val graph_w_edges = add_edges_from_andnodes_to_ornodes [and_key] graph_w_ornodes: abduction_graph;

• 3a. add or-to-and edges in

  PSL/Abduction/Proof_By_Abduction.ML

  Line 47 in 9084e8e

  val graph_w_ornodes_n_or2add_edges = fold (SOAN.add_or2and_edge or_key) seeds_of_newly_added_andnodes graph_w_ornodes: abduction_graph;

  PSL/Abduction/Seed_Of_And_Node.ML

  Line 151 in 9084e8e

  |> PGraph.new_node (or2and_edge_key, or2and_edge_val)

• 3b. This function also connects the parental or-node to the labelled edge.
  

  PSL/Abduction/Seed_Of_And_Node.ML

  Line 152 in 9084e8e

  |> Update_Abduction_Graph.add_edge_acyclic_if_possible or_key or2and_edge_key

• 3c. This function also connects the labelled edge to the and-node.
  

  PSL/Abduction/Seed_Of_And_Node.ML

  Line 152 in 9084e8e

  |> Update_Abduction_Graph.add_edge_acyclic_if_possible or_key or2and_edge_key

• 3d. cut edges to and-nodes inside add_or2and_edge in Seed_Of_And_Node.ML

  PSL/Abduction/Seed_Of_And_Node.ML

  Line 155 in 9084e8e

  val result = cut_edge_to_andnode_if_no_parental_ornode_can_be_proved_assmng_subgoals andnode_key or2and_edge_key graph_w_or2and_edge_connected;

Should we also cut edges to the or-nodes that represent conjectures that are not used in SH's output?

We simplified this in 962cca6.

from psl.

Problem: we have two problems at once:

• Results of tactic applications (implicit conjecturing) tend to contain multiple sub-goals in one and-node, where all sub-goals have to satisfy heuristics.
• Results of explicit conjecturing tend to consist of one conjecture each, but often we need multiple conjectures to solve the current sub-goal. So, we need to make sets of explicit conjectures, some of which may have already been proved or refuted.

from psl.

The bad thing about the current implementation is that filtering of conjectures is happening in two different locations:

• in top_down_conjectures in All_Top_Down_Conjecturing.ML, and
• n condition_to_filter_out in Seed_Of_Or2And_Edge.ML via filter_out_bad_seeds_of_or2and_edge and expand_ornode.

from psl.

Are SeLFiE-based filters useful only for explicit conjectures?

Maybe. -> counter example:

https://github.com/data61/PSL/blob/e7b482050f742bcc81d70a5068741e3527794ca0/Abduction/Seed_Of_Or2And_Edge.ML#LL120C16-L120C16

Anyways, the application of filtering should happen at the same place where implicit conjecturing also takes place for clarity.

from psl.

But the return type of apply_PSL_to_get_seeds_of_or2and_edges has to be seeds_of_or2and_edge because we need the resulting proof states after applying tactics.

This means that we have to apply filtering either

• to conjectures of type term within apply_PSL_to_get_seeds_of_or2and_edges or
• to terms inside seeds_of_or2and_edge after calling apply_PSL_to_get_seeds_of_or2and_edges.

I guess the latter will make the overall workflow easier to understand.

from psl.

At the same time, I should probably apply filtering functions to terms while constructing seeds not after constructing seeds because we have different treatments for terms for explicit/implicit conjecturing:

• for implicit conjecturing by tactic applications, we often have to check if all terms satisfy conditions, while
• for explicit conjecturing, we have to discard terms that do not satisfy conditions and construct a set of conjectures by collecting terms that passed the conditions.

from psl.

We need decremental conjecturing only for explicit conjecturing.

The algorithm is something like

fun identify_useful_conjectures (conjectures, accumulator) := {
  assume conjectures;
  try to prove the current goal;
  if proved using used_conjectures
  then 
    conjectures := conjectures - used_conjectures;
    identify_useful_conjectures (conjectures, used_conjectures @ accumulator)
 else
    accumulator
}

identify_useful_conjectures (explicit_conjectures, [ ]);

from psl.

identify_useful_conjectures is difficult to parallelise for each or-node.

But after the first iteration, we should have many or-nodes to handle (in parallel).

from psl.

We need decremental conjecturing only for explicit conjecturing.

The algorithm is something like

fun identify_useful_conjectures (conjectures, accumulator) := {
  assume conjectures;
  try to prove the current goal;
  if proved using used_conjectures
  then 
    conjectures := conjectures - used_conjectures;
    identify_useful_conjectures (conjectures, used_conjectures @ accumulator)
 else
    accumulator
}

identify_useful_conjectures (explicit_conjectures, [ ]);

I should not remove all the used conjectures at once like: conjectures := conjectures - used_conjectures;
Instead of that, I should create sets of conjectures, in each of which one used_conjecture is removed from the previous conjectures.

from psl.