We investigate the problem of finding optimal axiomatizations for operators and distribution quantifiers in finitely-valued first-order logics. We show that the problem can be viewed as the minimization of certain two-valued propositional formulas. We otuline a general procedure leading to optimized quantifier rules for the sequent calculus, for natural deduction and for clause formation. In the cae of operators and quantifiers based on semi-lattices, rules with a minimal branching degree can be obtained by instantitating a schema, which can also be used for optimal tableaux with sets-as-signs.
展开▼
