A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)

DOI10.1007/978-3-030-51054-1_2OpenAlexW3040077591MaRDI QIDQ5048990FDOQ5048990

Anne Baanen

Publication date: 9 November 2022

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_2

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• The Lean Theorem Prover (System Description)
• Isabelle/HOL. A proof assistant for higher-order logic
• Theorem Proving in Higher Order Logics
• Extending a Resolution Prover for Inequalities on Elementary Functions

Uses Software

• Coq
• Isabelle/HOL
• HOL Light
• Agda
• Lean

This page was built for publication: A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)

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