scientific article; zbMATH DE number 3871342

MaRDI QIDQ3338233zbMATH OpenFDO

Authors Frank Pfenning

Publication date 1984

zbMATH Keywords

algorithmanalytic proofsnatural deductionnon-analytic proofnon-resolution theorem provingtree expansion proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Recommendations

• scientific article; zbMATH DE number 956475
• PROOF-THEORETIC METHODS IN NONLINEAR ANALYSIS
• Mathematical analysis and proof
• scientific article; zbMATH DE number 1105739
• Proof-analysis and continuity
• Writing Proofs in Analysis
• scientific article; zbMATH DE number 1222925
• Analytic methods for the logic of proofs
• scientific article; zbMATH DE number 1090029
• An introduction to proof through real analysis

Cited in

(13)

• TPS: A theorem-proving system for classical type theory
• Translation of resolution proofs into short first-order proofs without choice axioms
• Writing Proofs in Analysis
• Semi-intelligible Isar proofs from machine-generated proofs
• The possibility of analysis: convergence and proofs of convergence
• scientific article; zbMATH DE number 956475 (Why is no real title available?)
• scientific article; zbMATH DE number 2090323 (Why is no real title available?)
• Mechanizing Mathematical Reasoning
• Presenting intuitive deductions via symmetric simplification
• Toward mechanical methods for streamlining proofs
• The TPS theorem proving system
• Extraction of expansion trees
• On connections and higher-order logic

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 Q3338233)