Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5477649
DOI10.1007/11541868zbMATH Open1152.68702OpenAlexW2484880499MaRDI QIDQ5477649FDOQ5477649
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)
Cited In (18)
- Formal Proofs for Nonlinear Optimization
- Title not available (Why is that?)
- Refinement to certify abstract interpretations: illustrated on linearization for polyhedra
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Incorporating quotation and evaluation into Church's type theory
- Towards a certified version of the encyclopedia of triangle centers
- A certificate-based approach to formally verified approximations
- MetiTarski: An automatic theorem prover for real-valued special functions
- Automatically proving equivalence by type-safe reflection
- Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
- Tactics for Reasoning Modulo AC in Coq
- Certifying compilers using higher-order theorem provers as certificate checkers
- A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)
- Formalization of Wu’s Simple Method in Coq
- A Formalization of Polytime Functions
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq
- What is the point of computers? A question for pure mathematicians
Uses Software
Recommendations
This page was built for publication: Theorem Proving in Higher Order Logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5477649)
