Yes. Been there, done that, with the pre-ACL2 Boyer-Moore prover. We had the Opp... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		Animats 3 days ago \| parent \| context \| favorite \| on: 50 years of proof assistants Yes. Been there, done that, with the pre-ACL2 Boyer-Moore prover. We had the Oppen-Nelson prover (the first SAT solver) handling the easy stuff, and used the Boyer-Moore prover for the hard stuff. Not that much manual work.

porcoda 3 days ago [–]

I assume you mean first SMT solver when you refer to Oppen-Nelson? I thought their contribution was the basis for SMT methods.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact