On the complexity of proof deskolemization

DOI10.2178/jsl/1333566645zbMath1345.03104OpenAlexW2129156376MaRDI QIDQ2892685

Matthias Baaz, Stefan Hetzl, Daniel Weller

Publication date: 19 June 2012

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.jsl/1333566645

zbMATH Keywords

Skolemizationcut-free proofslength of the shortest proof

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items (8)

Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \) ⋮ Andrews Skolemization may shorten resolution proofs non-elementarily ⋮ Algorithmic introduction of quantified cuts ⋮ Effective Skolemization ⋮ Unnamed Item ⋮ UNSOUND INFERENCES MAKE PROOFS SHORTER ⋮ Cut-elimination: syntax and semantics ⋮ Induction and Skolemization in saturation theorem proving

Cites Work

• Unnamed Item
• A compact representation of proofs
• Cut normal forms and proof complexity
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• Untersuchungen über das logische Schliessen. II
• Eliminating definitions and Skolem functions in first-order logic
• Cut-elimination and redundancy-elimination by resolution

This page was built for publication: On the complexity of proof deskolemization