Abduction: decremental conjecture identification in each layer.

[yutakang]

Instead of trying to identify one useful conjecture using Abductive reasoning, we can test many conjectures at once.

That is, we create and_node that contains all the explicit conjectures that are not refuted.

[yutakang]

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

[yutakang]

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.

[yutakang]

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 https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Proof_By_Abduction.ML#L44
• 2b This function also adds edges from the and-node to its child-or-nodes. https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Update_Abduction_Graph.ML#L220
• 3a. add or-to-and edges in https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Proof_By_Abduction.ML#L47 https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L151
• 3b. This function also connects the parental or-node to the labelled edge. https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L152
• 3c. This function also connects the labelled edge to the and-node. https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L152
• 3d. cut edges to and-nodes inside add_or2and_edge in Seed_Of_And_Node.ML https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L155

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

[yutakang]

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 https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Proof_By_Abduction.ML#L44
• 2b This function also adds edges from the and-node to its child-or-nodes. https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Update_Abduction_Graph.ML#L220

• 3a. add or-to-and edges in https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Proof_By_Abduction.ML#L47

  https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L151

• 3b. This function also connects the parental or-node to the labelled edge. https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L152
• 3c. This function also connects the labelled edge to the and-node. https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L152
• 3d. cut edges to and-nodes inside add_or2and_edge in Seed_Of_And_Node.ML https://github.com/data61/PSL/blob/9084e8e5dd270c0d1e3fbdc46823e534c4bbb006/Abduction/Seed_Of_And_Node.ML#L155

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

We simplified this in 962cca6e5abd996d40eccd403d683374f68aff5f.

[yutakang]

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.

[yutakang]

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.

[yutakang]

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.

[yutakang]

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.

[yutakang]

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.

[yutakang]

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, [ ]);

[yutakang]

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).

[yutakang]

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.

[yutakang]

I have to work on add_or2and_edge_and_connect_it_to_parental_ornode in Seed_Of_Or2And_Edge.ML

... because it is called in add_then_connect_or2and_edge_andnd_ornds.

[yutakang]

Currently, the return type of add_or2and_edge_and_connecdt_it_to_parental_ornode is

Abduction_Graph.key option *
(string * term) list *
 Abduction_Graph.abduction_graph

but this should be

Abduction_Graph.key option *
(string * term) list list * 
Abduction_Graph.abduction_graph

[yutakang]

Currently, the return type of add_or2and_edge_and_connecdt_it_to_parental_ornode is

Abduction_Graph.key option *
(string * term) list *
 Abduction_Graph.abduction_graph

but this should be

Abduction_Graph.key option *
(string * term) list list * 
Abduction_Graph.abduction_graph

This is probably not good enough.

[yutakang]

I have to change the type of seed_of_or2and_edge from

type seed_of_or2and_edge =
     {new_goals: terms,
      proof    : how_to_get_andnodes_from_ornode,
      state    : Proof.state};

to

type seed_of_or2and_edge =
     {new_goals: (string * term) list,
      proof    : how_to_get_andnodes_from_ornode,
      state    : Proof.state};

This change is desirable for decremental abduction.

Currently, we are attaching names to conjectures within add_or2and_edge_and_connect_it_to_parental_ornode in Seed_Of_Or2And_Edge.ML.

But this is inappropriate because we use the same term in different or2and_edge especially when using decremental abduction.

[yutakang]

I have to improve add_then_connect_or2and_edge_andnd_ornds in Seed_Of_Or2And_Edge.ML.

[yutakang]

I have to improve add_then_connect_or2and_edge_andnd_ornds in Seed_Of_Or2And_Edge.ML.

The new version of this function should support recursive calls. The recursive call would be a little odd, though: for each iteration

• we have to keep expanding the same abduction graph sequentially,
• we remove one previously used conjecture from seed_of_or2and_edge,
• we may return multiple new seeds (each lacking a conjecture used in the previous step),
• the recursion stops when we cannot prove the goal assuming the remaining conjectures.

[yutakang]

This was done a while ago.