On the complexity of proof deskolemization
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 627412
- scientific article; zbMATH DE number 3313427
- A surprising relationship between descriptive complexity and proof complexity
- scientific article; zbMATH DE number 1189101
- The proof complexity of SMT solvers
- The Complexity of Propositional Proofs
- The Complexity of Propositional Proofs
- scientific article; zbMATH DE number 1860672
- scientific article; zbMATH DE number 1156870
- scientific article; zbMATH DE number 2110622
Cites work
- A compact representation of proofs
- Cut normal forms and proof complexity
- Cut-elimination and redundancy-elimination by resolution
- Eliminating definitions and Skolem functions in first-order logic
- scientific article; zbMATH DE number 1497485 (Why is no real title available?)
- The liberalized -rule in free variable semantic tableaux
- Untersuchungen über das logische Schliessen. II
Cited in
(14)- Skolem functions of arithmetical sentences.
- Induction and Skolemization in saturation theorem proving
- Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
- Andrews Skolemization may shorten resolution proofs non-elementarily
- Cut-elimination: syntax and semantics
- scientific article; zbMATH DE number 7447752 (Why is no real title available?)
- Algorithmic introduction of quantified cuts
- scientific article; zbMATH DE number 627412 (Why is no real title available?)
- Unsound inferences make proofs shorter
- Effective Skolemization
- Interoperability of proof systems with SC-TPTP
- A generic deskolemization strategy
- A simplified proof of the epsilon theorems
- Epsilon calculus provides shorter cut-free proofs
This page was built for publication: On the complexity of proof deskolemization
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2892685)
