lawrencecpaulson / lawrencecpaulson.github.io

the blog "Machine Logic"

13 stars 0 forks source link

https://lawrencecpaulson.github.io/2022/08/17/Gordon-BDDs-HOL.html #19

Open utterances-bot opened 2 years ago

utterances-bot commented 2 years ago

BDDs in HOL: the coolest thing Mike Gordon ever did

https://lawrencecpaulson.github.io/2022/08/17/Gordon-BDDs-HOL.html

mn200 commented 2 years ago

I wonder a little about the characterisation of the approach as "extending the kernel". I think it's more accurate to say that we tagged the BDD theorems as trusted. The kernel code has a mechanism for oracles, and so we just used that. See the code at github

lawrencecpaulson commented 2 years ago

The “theorems” resulting from these extensions contain actual BDDs. The code seems to be defining a second kernel, one for BDDs. Then an oracle could transfer results from these BDD-thms to ordinary thms. Is that more accurate?

mn200 commented 2 years ago

Yes, that’s a nice way of putting it.