3.10 Tableaux Algorithm for ALC

[@richu-21]

Clear and on point Explanation. Thank you!

[@xhakil26]

Thank you

[@richu-21]

I think the video gets repeated after 28:18 as it is same as 24:42.

[@einkanal591]

Is it not a failure at 29:29 to use the TBox directly? Why is the conversion step of the axiom to NNF missing?

[@aleksandrakapa]

On for-every rule, if we have {R(a,a),(for every)R.B(a)} then do we use the rule? Or should we have R(a,b) a different from b?