Andrews Skolemization may shorten resolution proofs non-elementarily

DOI10.1007/978-3-030-93100-1_2OpenAlexW4200106768MaRDI QIDQ2151391

Anela Lolic, Matthias Baaz

Publication date: 1 July 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-93100-1_2

zbMATH Keywords

sequent calculusresolutionSkolemization

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items (1)

Effective Skolemization

Cites Work

• Unnamed Item
• Unnamed Item
• Lower bounds for increasing complexity of derivations after cut elimination
• On the complexity of proof deskolemization
• Theorem Proving via General Matings
• Lower Bounds on Herbrand's Theorem
• UNSOUND INFERENCES MAKE PROOFS SHORTER
• Resolution in type theory

This page was built for publication: Andrews Skolemization may shorten resolution proofs non-elementarily