Abduction: Parallel Sledgehammer

[yutakang]

Similar to parallel quickcheck.

• [ ] To prove multiple or-nodes, assuming conjectures.
  • This can be done by applying add_or2and_edge defined Proof_By_Abduction_Util.ML in parallel.
  • We have to split and_or2and_edge into two parts:
  • one for possibly getting the proof script,
  • the other for adding or cutting the edge.
• [ ] To prove each or-node completely.
  • This turns out to be a little trickier because it appears inside work_on_ornode in the loop in Proof_By_Abduction.
  • There seems to be a trade-off between an early break-out and parallelism.
  • I believe in parallelism.

[yutakang]

We probably need to use explicit synchronisation and introduce a new structure for that.

[yutakang]

We are not going to fold over proof_graph.

Instead, we use Synchronized.var and Par_List.exists: ('a -> bool) -> 'a list -> bool.

[yutakang]

Done. Parallel process of expand-or-nodes.