Abduction: should we pass around new `Proof.state` that contain proved conjectures?

data61 / PSL

Other

65 stars 9 forks source link

Abduction: should we pass around new `Proof.state` that contain proved conjectures? #198

Closed yutakang closed 11 months ago

yutakang commented 1 year ago

Probably we should not do so for the following reasons:

We can assume and register proved conjectures using the original Proof.state and abduction_graph.
Having two data structures (Proof.state and abduction_graph) is redundant.
It is better to focus on abduction_graph since we exploit parallelism.

yutakang commented 1 year ago

relaxed proof-state mode to take advantage of parallel branches in abduction graph in the presence of parallelism.

yutakang commented 11 months ago

No. We should not pass around Proof.state because we want to deal with conjectures explicitly: when we bury proved conjectures in the proof context, reasoning over such conjectures becomes harder.