Equational reasoning in Isabelle

DOI10.1016/0167-6423(89)90038-5zbMath0683.68081OpenAlexW1980290268MaRDI QIDQ1825045

Tobias Nipkow

Publication date: 1989

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0167-6423(89)90038-5

zbMATH Keywords

theorem provingequational logicreasoning

Mathematics Subject Classification ID

Related Items

Semi-intelligible Isar proofs from machine-generated proofs ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Term rewriting and beyond -- theorem proving in Isabelle ⋮ Tactics for Reasoning Modulo AC in Coq ⋮ The practice of logical frameworks