Resolution is one of the most elegant and powerful ideas in logic. It underlies a lot of early work in AI and nowadays it's used in many automated reasoning tools, such as in automated theorem proving. In this video, we're going to cover what resolution is, how it works, what you can do with it, where it came from and why it matters.
You can support the channel and help it grow by contributing on my Ko-fi page: https://ko-fi.com/atticphilosophy
00:00 - Intro
00:28 - What is Resolution?
02:40 - Resolution and Modus Ponens
03:50 - Where did resolution come from?
05:45 - Conjunctive Normal Form
06:58 - Refutation proofs
11:21 - Resolution in Automated Theorem Proving
If there’s a topic you’d like to see covered, leave me a comment below.
Links:
My academic philosophy page: http://markjago.net
My book What Truth Is: http://bit.ly/JagoTruth
Most of my publications are available freely here: https://philpapers.org/s/Mark%20Jago
#logic #proof #automatedreasoning #computerscience
