scientific article; zbMATH DE number 1259143
From MaRDI portal
Publication:4231030
zbMath0932.68099MaRDI QIDQ4231030
No author found.
Publication date: 9 March 1999
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Symbolic computation and algebraic computation (68W30) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
A Formalization of Properties of Continuous Functions on Closed Intervals, The gauge integral theory in HOL4, Formalization of linear space theory in the higher-order logic proving system, Formal Analysis of Optical Waveguides in HOL, Formal Verification of Exact Computations Using Newton’s Method, Wave equation numerical resolution: a comprehensive mechanized proof of a C program, Formalizing an analytic proof of the prime number theorem, Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation, Economic reasoning with demand and supply graphs, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, A few exercises in theorem processing, An approach for lifetime reliability analysis using theorem proving, Inversive meadows and divisive meadows, Verification of distributed systems with local-global predicates, Formal reasoning about finite-state discrete-time Markov chains in HOL, Formalization of real analysis: a survey of proof assistants and libraries, Unnamed Item, Applications of real number theorem proving in PVS, Rewriting with equivalence relations in ACL2, A Formalized Theory for Verifying Stability and Convergence of Automata in PVS, Certified Exact Transcendental Real Number Computation in Coq, Formal analysis of optical systems, Decision algorithms for fragments of real analysis. I: Continuous functions with strict convexity and concavity predicates, Survey article: The real numbers -- a survey of constructions, Proof synthesis and reflection for linear arithmetic, Reasoning about conditional probabilities in a higher-order-logic theorem prover, The control layer in open mechanized reasoning systems: Annotations and tactics, Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays, Formal verification of tail distribution bounds in the HOL theorem prover, Formalization of the standard uniform random variable, Meadows and the equational specification of division, Verified interactive computation of definite integrals, Formal proofs for theoretical properties of Newton's method, Building Mathematics-Based Software Systems to Advance Science and Create Knowledge, Combining Equational Reasoning, Using theorem proving to verify expectation and variance for discrete random variables, Performance analysis and functional verification of the stop-and-wait protocol in HOL, Mechanizing Nonstandard Real Analysis, On the formalization of gamma function in HOL, Implementing exact real arithmetic in python, C++ and C
Uses Software
