Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker

DOI10.1007/S10703-022-00391-XMaRDI QIDQ6661748FDOQ6661748

Authors: Daniela Kaufmann, Mathias Fleury, Armin Biere, M. Kauers 

Publication date: 13 January 2025

Published in: Formal Methods in System Design (Search for Journal in Brave)

Recommendations

• Proof certificates for algebra and their application to automatic geometry theorem proving
• Efficient verified (UN)SAT certificate checking
• Incremental column-wise verification of arithmetic circuits using computer algebra
• Algebraic proof systems over formulas.
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

zbMATH Keywords

Isabelle/HOLpolynomial calculusalgebraic proof systemsarithmetic circuit verificationGröbner basisNullstellensatz proofs

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Title not available (Why is that?)
• Isabelle/HOL. A proof assistant for higher-order logic
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• Using Gröbner bases to reason about geometry problems
• Semi-intelligible Isar proofs from machine-generated proofs
• The relative complexity of NP search problems
• The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them?
• Lower bounds for the polynomial calculus and the Gröbner basis algorithm
• Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
• Space Complexity in Propositional Calculus
• Code generation via higher-order rewrite systems
• Refinement to Imperative/HOL
• Producing and verifying extremely large propositional refutations
• Efficient certified RAT verification
• Nullstellensatz-proofs for multiplier verification
• A generalized method for proving polynomial calculus degree lower bounds
• Efficient, verified checking of propositional proofs
• Nullstellensatz size-degree trade-offs from reversible pebbling
• Title not available (Why is that?)
• Title not available (Why is that?)
• What can (and can't) we do with sparse polynomials?
• Local search for fast matrix multiplication
• New ways to multiply \(3 \times 3\)-matrices

Cited In (1)

• Certified verification for algebraic abstraction

This page was built for publication: Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6661748)