核心概念
Generalizing proof simulation procedures for Frege systems to Lukasiewicz logics.
要約
The content discusses the generalization of proof simulation procedures from Frege systems to Lukasiewicz logics, focusing on finite-valued Lukasiewicz logics. It presents new proof systems L3n∨ and L3∨, upper bounds on speed-ups, and comparisons with natural deduction and hypersequent calculus.
- Introduction
- Proof simulation in complexity theory.
- Cook and Reckhow's results on classical logic.
- Degrees of Polynomials
- Comparing efficiency of different calculi.
- Discrepancy between size and steps in proofs.
- Finite-Valued Lukasiewicz Logics
- Lack of deduction theorem in L3.
- Construction of ND-like calculus for L3.
- Simulation Procedures
- Bonet and Buss's simulation procedures for Frege systems.
- Generalization Results
- Upper bounds on speed-ups for natural deduction over Frege systems.
統計
一定のcがあると仮定すると、BがnステップでFregeシステムから導かれる場合、A ⊃ Bにはc·nステップでFrege証明が存在します。
BがA1、...、AmからnステップでFregeシステムで導かれた場合、A1 ⊃(...)⊃(Am ⊃ B)にはO(m + n)ステップのFrege証明が存在します。