On the desirability of mechanizing calculational proofs

DOI10.1016/S0020-0190(00)00200-3zbMath1003.68150OpenAlexW1980636983MaRDI QIDQ1607098

Panagiotis Manolios, J. Strother Moore

Publication date: 25 July 2002

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0020-0190(00)00200-3

zbMATH Keywords

calculational proofs

Mathematics Subject Classification ID

Related Items (3)

Computing and the cultures of proving ⋮ Equational abstractions ⋮ A Coq Library for Verification of Concurrent Programs

Uses Software

• ACL2
• ML
• OTTER
• PVS
• HOL

Cites Work

• The varieties of arboreal experience
• A program refinement tool
• Metamathematics, Machines and Gödel's Proof
• On calculational proofs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the desirability of mechanizing calculational proofs