Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5477649
DOI10.1007/11541868zbMath1152.68702OpenAlexW2484880499MaRDI QIDQ5477649
Benjamin Grégoire, Assia Mahboubi
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
Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)
Related Items
Automatically proving equivalence by type-safe reflection, Towards a certified version of the encyclopedia of triangle centers, A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper), Unnamed Item, Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra, Extending a Resolution Prover for Inequalities on Elementary Functions, What is the point of computers? A question for pure mathematicians, Certifying compilers using higher-order theorem provers as certificate checkers, A certificate-based approach to formally verified approximations, Refinement to certify abstract interpretations: illustrated on linearization for polyhedra, Incorporating quotation and evaluation into Church's type theory, MetiTarski: An automatic theorem prover for real-valued special functions, A Formalization of Polytime Functions, Formalization of Wu’s Simple Method in Coq, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, Tactics for Reasoning Modulo AC in Coq, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Formal Proofs for Nonlinear Optimization
Uses Software
