ʊ-resolution: An inference rule for regular multiple-valued logics

Abstract

The inference rule ʊ-resolution for regular multiple-valued logics is developed. One advantage of ʊ-resolution is that linear, regular proofs are possible. That is, unlike existing deduction techniques, ʊ-resolution admits input deductions (for Horn sets) while maintaining regular signs. More importantly, ʊ-resolution proofs are at least as short as proofs for definite clauses generated by the standard inference techniques—annotated resolution and reduction—and pruning of the search space occurs automatically.