Enabling symbolic and numerical computations in HOL Light

DOI10.1007/978-3-319-20615-8_27MaRDI QIDQ3453133zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 1254246 (Why is no real title available?)
• scientific article; zbMATH DE number 1497742 (Why is no real title available?)
• scientific article; zbMATH DE number 1863375 (Why is no real title available?)
• 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
• Formal analysis of optical systems

Cited in

(4)

• HOL Light QE
• scientific article; zbMATH DE number 517013 (Why is no real title available?)
• Steps towards Verified Implementations of HOL Light
• A bi-directional extensible interface between Lean and Mathematica

Describes a project that uses

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)