Enabling symbolic and numerical computations in HOL Light

DOI10.1007/978-3-319-20615-8_27zbMATH Open1417.68193OpenAlexW1147542396MaRDI QIDQ3453133FDOQ3453133

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

Recommendations

• Certified Computer Algebra on Top of an Interactive Theorem Prover
• scientific article; zbMATH DE number 517013
• A Skeptic's approach to combining HOL and Maple
• HOL Light: An Overview
• scientific article; zbMATH DE number 1863375

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• A Skeptic's approach to combining HOL and Maple
• Formal analysis of optical systems
• Title not available (Why is that?)
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• Analytica --- an experiment in combining theorem proving and symbolic computation
• Title not available (Why is that?)

Cited In (3)

• Steps towards Verified Implementations of HOL Light
• Title not available (Why is that?)
• A bi-directional extensible interface between Lean and Mathematica

Uses Software

• Mathematica
• Theorema
• HOL Light
• Analytica

This page was built for publication: Enabling symbolic and numerical computations in HOL Light

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453133)