On Theorem Proving in Annotated Logics Academic Article uri icon


  • 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 Mstrategy 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.

published proceedings

  • Journal of Applied Non-Classical Logics

author list (cited authors)

  • Lu, M. i., & Wu, J.

complete list of authors

  • Lu, Mi||Wu, Jinzhao

publication date

  • January 1, 2000 11:11 AM