Abduction: something is wrong about adding and-nodes. about psl HOT 6 CLOSED

Maybe we have to strengthen ...

• cycle detection.

I also probably assumed uniqueness of and-node.

from psl.

Quick fix in f9ae390.

Is this enough?

from psl.

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:

from psl.

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.

from psl.

Quick fix in f9ae390.

Is this enough?

Probably not.

How are duplicated nodes are handled?

What if the duplicated nodes are already proved?

from psl.

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.

from psl.