On Theorem Proving in Annotated Logics
Mi Lu, Jinzhao Wu · Journal of Applied Non-Classical Logics · 2000
We are concerned with the theorem proving in annotated logics. By using annotated polynomials to express knowledge, we develop an inference rule superposition. A proof procedure is thus presented, and an improvement named M- strategy is mainly described. This proof procedure uses single overlaps instead of multiple overlaps, and above all, both the proof procedure and M-strategy are refutationally complete.