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

DOI10.1007/978-3-030-51054-1_2MaRDI QIDQ5048990OpenAlexFDO

Authors 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

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

Describes a project that uses

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)