C. Geissler, K. Konolige. Proc. of TARK'86, March 1986, California, USA.
Abstract: B-resolution is a sound and complete resolution rule for quantified modal logics of knowledge and belief with a standard Kripke semantics. It differs from ordinary first-order binary resolution in that it can have an arbitrary (but finite) number of inputs, is not necessarily effective, and does not have a most general unifier covering every instance of an application. These properties present obvious obstacles to implementation in an automatic theorem-proving system. By using a technique similar to semantic attachment, we obtain a very natural expression of B-resolution that is potentially efficient, and easily understood and controlled. We have implemented the method and used it to solve the Wise Man Puzzle.