Formalizing a Hierarchical Structure of Practical Mathematical Reasoning

DOI10.1093/LOGCOM/3.1.47MaRDI QIDQ4272504zbMATH OpenOpenAlexFDO

Authors Peter J. Robinson, John Staples

Publication date 6 December 1993

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/3.1.47

zbMATH Keywords

inference systemsinteractive reasoningequivalence proofsproof editors

Mathematics Subject Classification ID

Recommendations

• Hierarchical deduction
• scientific article; zbMATH DE number 1951638
• Proof planning: A practical approach to mechanized reasoning in mathematics
• Structured calculational proof
• scientific article; zbMATH DE number 4164180

Cited in

(13)

• Verifying Whiley programs with Boogie
• A Mizar mode for HOL
• A structure preserving encoding of Z in Isabelle/HOL
• Program derivation using the refinement calculator
• Using lattice theory in higher order logic
• Mathematical reasoning vs. abductive reasoning: A structural approach
• Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
• A proof-planning framework with explicit abstractions based on indexed formulas
• From Boolean algebra to unified algebra
• A functional logic for higher level reasoning about computation
• Structured calculational proof
• The Logical Structure of Computer-Aided Mathematical Reasoning
• Mathematical Knowledge Management

This page was built for publication: Formalizing a Hierarchical Structure of Practical Mathematical Reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4272504)