Unsound inferences make proofs shorter
From MaRDI portal
Publication:4628675
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.
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
Cites work
- scientific article; zbMATH DE number 627412 (Why is no real title available?)
- scientific article; zbMATH DE number 3334141 (Why is no real title available?)
- Cut normal forms and proof complexity
- Lower Bounds on Herbrand's Theorem
- Lower bounds for increasing complexity of derivations after cut elimination
- On the complexity of proof deskolemization
- On the non-confluence of cut-elimination
- The epsilon calculus and Herbrand complexity
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)
