Enabling Symbolic and Numerical Computations in HOL Light

DOI10.1007/978-3-319-20615-8_27zbMath1417.68193OpenAlexW1147542396MaRDI QIDQ3453133

Sofiène Tahar, Sanaz Khan-Afshar, Cvetan Dunchev, Ons Seddiki

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-20615-8_27

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Related Items (1)

A bi-directional extensible interface between Lean and Mathematica

Uses Software

• Mathematica
• Theorema
• HOL Light
• Analytica

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal analysis of optical systems
• A Skeptic's approach to combining HOL and Maple
• Analytica --- an experiment in combining theorem proving and symbolic computation
• Certified Computer Algebra on Top of an Interactive Theorem Prover

This page was built for publication: Enabling Symbolic and Numerical Computations in HOL Light