On Theorem Proving in Annotated Logics
Academic Article
Overview
Identity
Additional Document Info
Other
View All
Overview
abstract
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.