search

data61 / PSL

Other
65 stars 9 forks source link

Can we get rid of chained state from `seed_of_or2and_edge`? #211

Open yutakang opened 1 year ago

yutakang commented 1 year ago

Can we get rid of chained states from seed_of_or2and_edge?

Instead of passing a chained state that we obtain after applying certain proof methods, I would like to reconstruct such proof state by applying the methods.

https://github.com/data61/PSL/blob/d59677eaa34db88b728ae85114d913151df1c266/Abduction/Seed_Of_Or2And_Edge.ML#L44

yutakang commented 1 year ago

I need this change because the current implementation is breaking proofs here.

https://github.com/data61/PSL/blob/d59677eaa34db88b728ae85114d913151df1c266/Abduction/Top_Down_Util.ML#L221

I should be able to reconstruct proof using https://github.com/data61/PSL/blob/d59677eaa34db88b728ae85114d913151df1c266/PSL/Subtool.ML#L88.

https://github.com/data61/PSL/blob/d59677eaa34db88b728ae85114d913151df1c266/PSL/Subtool.ML#L88