Equational reasoning via partial reflection

DOI10.1007/3-540-44659-1_11MaRDI QIDQ2754042zbMATH OpenFDO

Authors Herman Geuvers, Freek Wiedijk, Jan Zwanenburg

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44659-1_11

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Types for Proofs and Programs
• Equational reasoning in Isabelle
• scientific article; zbMATH DE number 4155899
• Equational Reasoning with Applicative Functors
• scientific article; zbMATH DE number 1552533
• scientific article; zbMATH DE number 1552532
• Equational Reasoning in Non-Classical Logics
• scientific article; zbMATH DE number 1036757
• Equational logic as a tool
• Combining equational reasoning

Cited in

(8)

• A constructive algebraic hierarchy in Coq.
• Equational Reasoning with Applicative Functors
• A logical framework with explicit conversions
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Constrained equational deduction
• Types for Proofs and Programs
• Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Equational reasoning via partial reflection

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