TY - GEN
T1 - A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)
AU - Baanen, Anne
N1 - The final authenticated version is available online at https://doi.org/10.1007/978-3-030-51054-1_2.
PY - 2020
Y1 - 2020
N2 - This paper describes the design of the normalising tactic ring_exp for the Lean prover. This tactic improves on existing tactics by extending commutative rings with a binary exponent operator. An inductive family of types represents the normal form, enforcing various invariants. The design can also be extended with more operators.
AB - This paper describes the design of the normalising tactic ring_exp for the Lean prover. This tactic improves on existing tactics by extending commutative rings with a binary exponent operator. An inductive family of types represents the normal form, enforcing various invariants. The design can also be extended with more operators.
UR - http://www.scopus.com/inward/record.url?scp=85088234858&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85088234858&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-51054-1_2
DO - 10.1007/978-3-030-51054-1_2
M3 - Conference contribution
SN - 9783030510534
VL - 2
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 21
EP - 27
BT - Automated Reasoning
A2 - Peltier, Nicolas
A2 - Sofronie-Stokkermans, Viorica
PB - Springer
T2 - 10th International Joint Conference on Automated Reasoning, IJCAR 2020
Y2 - 1 July 2020 through 4 July 2020
ER -
