Theorem Proving in Higher Order Logics

DOI10.1007/11541868zbMath1152.68527OpenAlexW2484880499MaRDI QIDQ5477656

David R. Lester, César A. Muñoz

Publication date: 6 July 2006

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

Full work available at URL: https://doi.org/10.1007/11541868

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60)

Related Items

Computer-Aided Verification for Iterative Matrix Inversion Problems in Systems and Control, A verified ODE solver and the Lorenz attractor, Applications of real number theorem proving in PVS, Proving Bounds on Real-Valued Functions with Computations, Real Number Calculations and Theorem Proving, Certified Exact Transcendental Real Number Computation in Coq, Floating-point arithmetic in the Coq system

Uses Software

• PVS