scientific article; zbMATH DE number 3871341

MaRDI QIDQ3338232zbMATH OpenFDO

Authors Dale Miller

Publication date 1984

zbMATH Keywords

natural deduction proofsexpansion treesmatingsET-proofs

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Recommendations

• A compact representation of proofs
• Expansion trees with cut
• Extraction of expansion trees
• scientific article; zbMATH DE number 3922016
• On connections and higher-order logic

Cited in

(12)

• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• scientific article; zbMATH DE number 5136283 (Why is no real title available?)
• The TPS theorem proving system
• On connections and higher-order logic
• Presenting intuitive deductions via symmetric simplification
• TPS: A theorem-proving system for classical type theory
• TPS: A hybrid automatic-interactive system for developing proofs
• Toward mechanical methods for streamlining proofs
• A compact representation of proofs
• scientific article; zbMATH DE number 5000964 (Why is no real title available?)
• Trees and diagrams of decomposition
• Expansion trees with cut

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