Unsound inferences make proofs shorter

DOI10.1017/JSL.2018.51zbMATH Open1439.03095arXiv1608.07703OpenAlexW3101828175WikidataQ113858288 ScholiaQ113858288MaRDI QIDQ4628675FDOQ4628675

Authors: Juan P. Aguilera, Matthias Baaz 

Publication date: 15 March 2019

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

Abstract: We give examples of calculi that extend Gentzen's sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs.

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

Recommendations

• A Resolution Calculus for Shortening Proofs
• scientific article; zbMATH DE number 1324437
• The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
• Gentzen systems, resolution, and literal trees
• Proof generalization in \(\mathrm {LK}\) by second order unifier minimization

zbMATH Keywords

cut eliminationsequent calculuseigenvariable conditionunsound inferences

Mathematics Subject Classification ID

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

Cites Work

• The epsilon calculus and Herbrand complexity
• Lower bounds for increasing complexity of derivations after cut elimination
• Lower Bounds on Herbrand's Theorem
• On the complexity of proof deskolemization
• Title not available (Why is that?)
• Title not available (Why is that?)
• Cut normal forms and proof complexity
• On the non-confluence of cut-elimination

Cited In (14)

• Note on the benefit of proof representations by name
• Determinate logic and the axiom of choice
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
• Non-transitive correspondence analysis
• EPSILON THEOREMS IN INTERMEDIATE LOGICS
• Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
• Herbrand complexity and the epsilon calculus with equality
• The number of axioms
• Andrews Skolemization may shorten resolution proofs non-elementarily
• Sequent calculi for first-order ST
• Towards a proof theory for quantifier macros
• Some analytic systems of rules
• Effective Skolemization
• Computer Science Logic

This page was built for publication: Unsound inferences make proofs shorter

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