ROSCoq: Robots Powered by Constructive Reals

DOI10.1007/978-3-319-22102-1_3zbMath1465.68258OpenAlexW2147877794MaRDI QIDQ2945622

Ross A. Knepper, Abhishek Anand

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) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

ROSCoq

Uses Software

• Coq

Cites Work

• Unnamed Item
• Buridan's principle
• The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?
• Logics of Dynamical Systems
• Type classes for mathematics in type theory
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Time, clocks, and the ordering of events in a distributed system
• Type classes for efficient exact real arithmetic in Coq
• Automated Machine-Checked Hybrid System Safety Proofs

This page was built for publication: ROSCoq: Robots Powered by Constructive Reals