Topic: GENERAL LOGIC
Polynomial Ring Calculus for Logical Inference
By Walter Carnielli
This paper proposes a new "all-purpose" algebraic proof method applicable to general truth-functional sentential logics and to some non-truth-functional logics. The method, based on reducing polynomials over finite fields, is particularly apt for finitely-many-valued logics (and for classical propositional logic PC ). It can be extended to certain non-finitely valued logics and non-truth-functional logics as well, provided they can be characterized by two-valued dyadic semantics. The resulting mechanizable proof method introduced here is of interest for automatic proof theory, and seems also to be appropriate for investigating questions on complexity.
Posted by Tony Marmo at 20:14 BST
Updated: Sunday, 10 April 2005 20:16 BST