Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)

DOI10.1007/s00153-021-00798-zzbMath1506.03120arXiv1909.01697OpenAlexW3216042957MaRDI QIDQ2144618

Ján Komara

Publication date: 14 June 2022

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1909.01697

zbMATH Keywords

cut eliminationsequent calculusSkolem functionsproof complexityeigenvariable conditionHenkin constantsstrong locality property

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03) Complexity of proofs (03F20)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The predicate calculus with \(\varepsilon\)-symbol
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
• Proof theory. 2nd ed
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• On the complexity of proof deskolemization
• UNSOUND INFERENCES MAKE PROOFS SHORTER
• Eliminating definitions and Skolem functions in first-order logic
• Computer Science Logic
• The completeness of the first-order functional calculus