OpenMath and SMT-LIB
James H. Davenport, Matthew England, Roberto Sebastiani, Patrick, Trentin
TL;DR
This paper discusses the relationship between OpenMath and SMT-LIB, two languages for representing mathematics, and explores how SMT-LIB can be adapted for the OpenMath community and the SC-Square initiative.
Contribution
It provides a bridge between OpenMath and SMT-LIB, facilitating interoperability and supporting the SC-Square initiative through proposed adaptations.
Findings
SMT-LIB can be integrated with OpenMath for better interoperability
Proposed adaptations enhance support for the SC-Square initiative
The paper facilitates cross-language understanding of mathematical representations
Abstract
OpenMath and SMT-LIB are languages with very different origins, but both "represent mathematics". We describe SMT-LIB for the OpenMath community and consider adaptations for both languages to support the growing SC-Square initiative.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics, Computing, and Information Processing