scientific article; zbMATH DE number 627412
From MaRDI portal
Publication:4304753
Recommendations
Cited in
(44)- A solver for QBFs in negation normal form
- Describing proofs by short tautologies
- Complexity of resolution proofs and function introduction
- Elimination of Skolem functions for monotone formulas in analysis
- Cut normal forms and proof complexity
- On the compressibility of finite languages and formal proofs
- Skolemization and Herbrand theorems for lattice-valued logics
- Generalizing theorems in real closed fields
- A note on assumptions about Skolem functions
- Induction and Skolemization in saturation theorem proving
- Andrews Skolemization may shorten resolution proofs non-elementarily
- Ceres in intuitionistic logic
- Automation for interactive proof: first prototype
- Towards a clausal analysis of cut-elimination
- Translation of resolution proofs into short first-order proofs without choice axioms
- The Skolemization of existential quantifiers in intuitionistic logic
- Controlling witnesses
- A note on the size of prenex normal forms
- Schematic cut elimination and the ordered pigeonhole principle
- Skolemization modulo theories
- On the complexity of proof deskolemization
- Skolemization in simple type theory: the logical and the theoretical points of view
- scientific article; zbMATH DE number 4037813 (Why is no real title available?)
- Algorithmic introduction of quantified cuts
- scientific article; zbMATH DE number 1342207 (Why is no real title available?)
- Direct deductive computation on discourse representation structures
- Non-elementary speed-ups in proof length by different variants of classical analytic calculi
- Projection: a unification procedure for tableaux in conceptual graphs
- Unsound inferences make proofs shorter
- Eliminating definitions and Skolem functions in first-order logic
- Herbrand Sequent Extraction
- Efficient Skolemization
- Cut-elimination and redundancy-elimination by resolution
- Effective Skolemization
- On the elimination of quantifier-free cuts
- Extraction of expansion trees
- Non-elementary compression of first-order proofs in deep inference using epsilon-terms
- Antiprenexing for WSkS: a little goes a long way
- On translations of epsilon proofs to LK
- CERES in higher-order logic
- Epsilon calculus provides shorter cut-free proofs
- The epsilon calculus and Herbrand complexity
- CERES: An analysis of Fürstenberg's proof of the infinity of primes
- On the form of witness terms
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4304753)
