Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0

DOI10.1007/978-3-319-42432-3_8zbMath1434.68641OpenAlexW2495091588MaRDI QIDQ2819200

Alexander Maletzky

Publication date: 28 September 2016

Published in: Mathematical Software – ICMS 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-42432-3_8

zbMATH Keywords

interactive theorem provingTheoremacomputer-assisted mathematical theory exploration

Mathematics Subject Classification ID

Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isar
• Unnamed Item
• Unnamed Item
• Unnamed Item

Cites Work

• Mathematical Theory Exploration in Theorema: Reduction Rings
• Decidability of higher-order matching
• The Theorema Environment for Interactive Proof Development

This page was built for publication: Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0