Toward automating the discovery of decreasing measures

DOI10.1007/S10817-005-9020-ZzbMath1107.68094OpenAlexW1984585577MaRDI QIDQ861690

Robert S. Boyer, Victor W. Marek, Wilfred J. Legato

Publication date: 30 January 2007

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

Full work available at URL: https://doi.org/10.1007/s10817-005-9020-z

zbMATH Keywords

theorem-proving system

Mathematics Subject Classification ID

Uses Software

• ACL2
• NQTHM

Cites Work

• On the restricted ordinal theorem
• The consistency of arithmetics

This page was built for publication: Toward automating the discovery of decreasing measures