Systematic construction of natural deduction systems for many-valued logics
Matthias Baaz, Christian G. Fermüller, Richard Zach
Abstract
Open-access reader
Matthias Baaz, Christian G. Fermüller, Richard Zach
Abstract
Open-access reader
A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.>
OpenAlex reports 50 citations for this work. Citation counts describe recorded attention and do not establish research quality.
A contribution statement is not available in the OpenAlex record.
Method details are not available in the OpenAlex metadata.
Findings are not separately available in the OpenAlex metadata.
Limitations are not available in the OpenAlex metadata.
Application details are not available in the OpenAlex metadata.
A construction principle for natural deduction systems for arbitrary, finitely-many-valued first order logics is exhibited. These systems are systematically obtained from sequent calculi, which in turn can be automatically extracted from the truth tables of the logics under consideration. Soundness and cut-free completeness of these sequent calculi translate into soundness, completeness, and normal-form theorems for natural deduction systems.>
Key concepts: Sequent, Soundness, Natural deduction, Sequent calculus, Completeness (order theory), Cut-elimination theorem, Computer science, Automated theorem proving