scientific article; zbMATH DE number 627412

zbMath0815.03003MaRDI QIDQ4304753

Alexander Leitsch, Matthias Baaz

Publication date: 31 August 1994

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

proof complexitySkolemizationHerbrand complexityautomated theorem-proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Related Items

Ceres in intuitionistic logic, Generalizing theorems in real closed fields, Andrews Skolemization may shorten resolution proofs non-elementarily, Algorithmic introduction of quantified cuts, Effective Skolemization, Automation for interactive proof: first prototype, On the compressibility of finite languages and formal proofs, Non-elementary speed-ups in proof length by different variants of classical analytic calculi, Projection: A unification procedure for tableaux in Conceptual Graphs, On the elimination of quantifier-free cuts, UNSOUND INFERENCES MAKE PROOFS SHORTER, Towards a clausal analysis of cut-elimination, Extraction of expansion trees, CERES: An analysis of Fürstenberg's proof of the infinity of primes, Cut-elimination and redundancy-elimination by resolution, Translation of resolution proofs into short first-order proofs without choice axioms, On the form of witness terms, CERES in higher-order logic, The Skolemization of existential quantifiers in intuitionistic logic, Schematic Cut Elimination and the Ordered Pigeonhole Principle, A solver for QBFs in negation normal form, Describing proofs by short tautologies, Controlling witnesses, Induction and Skolemization in saturation theorem proving, Herbrand Sequent Extraction, Cut normal forms and proof complexity, The epsilon calculus and Herbrand complexity