Theorem Proving in Higher Order Logics

DOI10.1007/11541868MaRDI QIDQ5477649zbMATH OpenOpenAlexFDO

Authors 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

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)

Recommendations

• A refinement-based approach to computational algebra in Coq
• Dealing with algebraic expressions over a field in Coq using Maple
• Z-module reasoning
• scientific article; zbMATH DE number 1670742
• Automated proof of ring commutativity problems by algebraic methods

Cited in

(18)

• Formal Proofs for Nonlinear Optimization
• 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
• Formalization of Wu's simple method in Coq
• Automatically proving equivalence by type-safe reflection
• Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra
• A formalization of polytime functions
• A formal proof of the irrationality of \(\zeta(3)\)
• Modular SMT proofs for fast reflexive checking inside Coq
• 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)
• What is the point of computers? A question for pure mathematicians

Describes a project that uses

Uses Software

• Coq

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)