Proof Theory of Finite-Valued Logics Export

@mastersthesis{Zach:93, abstract = {Several people have, since the 1950's, proposed ways to generalize proof theoretic formalisms (sequent calculus, natural deduction, resolution) from the classical to the many-valued case. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order logics in a general way, and to present some of the more important results in this area. This report is actually a template, from which all results can be specialized to particular logics. The main results of this report are: the use of signed formula expressions and partial normal forms to provide a unifying framework in which clause translation calculi, sequent calculi, natural deduction, and also tableaux can be represented; bounds for partial normal forms for general and induced quantifiers; and negative resolution. The cut-elimination theorems extend previous results, and the midsequent theorem, natural deduction systems for many-valued logics as well as results on approximation of axiomatizable propositional logics by many-valued logics are all new.}, address = {Vienna}, author = {Zach, Richard}, citeulike-article-id = {129434}, citeulike-linkout-0 = {http://www.ucalgary.ca/~rzach/papers/ptmvl.html}, keywords = {logic, many-valued\_logic, natural\_deduction, proof\_theory, resolution, sequent\_calculus, tableaux}, posted-at = {2005-03-16 03:55:38}, priority = {0}, school = {Technische Universit\"{a}t Wien}, title = {Proof Theory of Finite-Valued Logics}, url = {http://www.ucalgary.ca/~rzach/papers/ptmvl.html}, year = {1993} }

TY - THES ID - Zach:93 L3 - citeulike-article-id:129434 N2 - Several people have, since the 1950's, proposed ways to generalize proof theoretic formalisms (sequent calculus, natural deduction, resolution) from the classical to the many-valued case. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order logics in a general way, and to present some of the more important results in this area. This report is actually a template, from which all results can be specialized to particular logics. The main results of this report are: the use of signed formula expressions and partial normal forms to provide a unifying framework in which clause translation calculi, sequent calculi, natural deduction, and also tableaux can be represented; bounds for partial normal forms for general and induced quantifiers; and negative resolution. The cut-elimination theorems extend previous results, and the midsequent theorem, natural deduction systems for many-valued logics as well as results on approximation of axiomatizable propositional logics by many-valued logics are all new. AD - Vienna TI - Proof Theory of Finite-Valued Logics PB - Technische Universität Wien KW - logic KW - many-valued_logic KW - natural_deduction KW - proof_theory KW - resolution KW - sequent_calculus KW - tableaux AU - Zach, Richard PY - 1993/// UR - http://www.ucalgary.ca/~rzach/papers/ptmvl.html ER -