Abduction: something is wrong about adding and-nodes.

[yutakang]

seeds_to_updated_graph is called in work_on_ornode.

seeds_to_updated_graph calls add_andnodes.

add_andnodes calls add_nodes.

new_node inside add_nodes ignores a key-abduction_node pair if the abduction graph already has an element for the key.

This means that once we add an and-node to the graph and assume that add-node for a particular or-node that is the parent of the and-node, we cannot use the and-node to prove other or-nodes....(?)

[yutakang]

Maybe we have to strengthen ...

• cycle detection.

I also probably assumed uniqueness of and-node.

[yutakang]

Quick fix in f9ae39008a6e624ae3a20d0ad6e976d2159d7a33.

Is this enough?

[yutakang]

If the and-node should be already flagged as "refuted", can we take advantage of this information?

Should we actually include refuted nodes in the graph even though we have introduced Shared_State, which tracks the refuted terms?

If we get rid of refuted nodes from abduction_graph, we can simplify this part: https://github.com/data61/PSL/blob/f9ae39008a6e624ae3a20d0ad6e976d2159d7a33/Abduction/Proof_By_Abduction.ML#L44.

[yutakang]

I was hoping to refute parental nodes using the information I could possibly get when refuting their descendants. Well... that was too much to implement.

Also, I was thinking of using multiple timeouts for counterexample finders and revisit the same nodes, for which counterexample finders have already timed out, with a longer timeout in the second time. This can be done without having refuted nodes in abduction_graph.

[yutakang]

Quick fix in f9ae390.

Is this enough?

Probably not.

How are duplicated nodes are handled?

What if the duplicated nodes are already proved?

[yutakang]

Maybe we have to strengthen ...

• cycle detection.

I also probably assumed uniqueness of and-node.

We should tolerate cycles. The abduction graph is not acyclic.