3 ms·
I don't agree. The derivation of new clauses by Resolution is well understood as deductive and the choice of what clauses to keep doesn't change that. Resoluti
by YeGoblynQueenne 2y ago
I don't agree. The derivation of new clauses by Resolution is well understood as deductive and the choice of what clauses to keep doesn't change that.
Resolution can be used inductively, and also for abduction, but that's going into the weeds a bit- it's the subject of my PhD thesis. Let me know if you're in the mood for a proper diatribe :)
- joe_the_user 2y agoI'd love a diatribe if you're still following this post.
- EarlKing 2y agoAs would I. You know, this seems like yet another reason to allow HN users to direct message each other, or at least receive reply notifications. Dang, why can't we have nice things?
- YeGoblynQueenne 2y agoOh, hi guys. Sorry just saw this. Oh gosh I gotta do some work today, so no time to write what I wanted. Maybe watch this space? I'll try to make some time later today.
- thesz 2y agoTake a look at Satisfaction-Driven Clause Learning [1]. [1] https://www.cs.cmu.edu/~mheule/publications/prencode.pdf https://www.cs.cmu.edu/~mheule/publications/prencode.pdf