Effective Skolemization

DOI10.1007/978-3-031-39784-4_5MaRDI QIDQ6118680zbMATH OpenOpenAlexFDO

Authors Matthias Baaz, Anela Lolic

Publication date 28 February 2024

Published in Logic, Language, Information, and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-39784-4_5

zbMATH Keywords

cut-free proofsresolution proofsSkolemization

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites work

• Andrews Skolemization may shorten resolution proofs non-elementarily
• Cut normal forms and proof complexity
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• Lower Bounds on Herbrand's Theorem
• Methods of cut-elimination
• On the complexity of proof deskolemization
• Resolution in type theory
• Theorem Proving via General Matings
• Unsound inferences make proofs shorter

Cited in

(1)

• Epsilon calculus provides shorter cut-free proofs

This page was built for publication: Effective Skolemization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6118680)