ROSCoq: robots powered by constructive reals

DOI10.1007/978-3-319-22102-1_3MaRDI QIDQ2945622zbMATH OpenOpenAlexFDO

Authors Abhishek Anand, Ross A. Knepper

Publication date 14 September 2015

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-22102-1_3

Mathematics Subject Classification ID

Artificial intelligence for robotics (68T40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Computer Certified Efficient Exact Reals in Coq
• Automated Machine-Checked Hybrid System Safety Proofs
• A certified, corecursive implementation of exact real numbers
• Commanding a robot in a safe way
• Type classes for efficient exact real arithmetic in \textsc{Coq}

Cites work

• Automated Machine-Checked Hybrid System Safety Proofs
• Buridan's principle
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Logics of dynamical systems
• The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them?
• Time, clocks, and the ordering of events in a distributed system
• Type classes for efficient exact real arithmetic in \textsc{Coq}
• Type classes for mathematics in type theory

Cited in

(5)

• ROSCoq
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• Towards constructive hybrid semantics
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
• Formally verifying a vertical cell decomposition algorithm

Describes a project that uses

Uses Software

• Coq

This page was built for publication: ROSCoq: robots powered by constructive reals

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