Satisfiability modulo finite fields

DOI10.1007/978-3-031-37703-7_8zbMATH Open1545.68086MaRDI QIDQ6535532FDOQ6535532

Gereon Kremer, Clark Barrett, Alex Ozdemir, Cesare Tinelli

Publication date: 12 January 2024

Mathematics Subject Classification ID

Finite fields (field-theoretic aspects) (12E20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Magma algebra system. I: The user language
• CoCoALib: A C++ Library for Computations in Commutative Algebra... and Beyond
• Computations in algebraic geometry with Macaulay 2
• SINGULAR
• SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
• The Lean Theorem Prover (System Description)
• The MathSAT5 SMT Solver
• A new efficient algorithm for computing Gröbner bases \((F_4)\)
• A mathematical introduction to logic.
• The knowledge complexity of interactive proof-systems
• Efficient computation of zero-dimensional Gröbner bases by change of ordering
• Solving SAT and SAT Modulo Theories
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Solving Non-linear Arithmetic
• A Model-Constructing Satisfiability Calculus
• Cutting to the Chase Solving Linear Integer Arithmetic
• Automated deduction for verification
• On the theories of triangular sets
• Probabilistic Algorithms in Finite Fields
• Secure Multiparty Computation Goes Live
• Quantifier elimination for real algebra -- the quadratic case and beyond
• A new method for solving algebraic systems of positive dimension
• Computation of Hilbert functions
• Solving zero-dimensional algebraic systems
• SMT-based scenario verification for hybrid systems
• A Machine-Checked Proof of the Odd Order Theorem
• Formalizing Some “Small” Finite Models of Projective Geometry in Coq
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
• Solving Nonlinear Integer Arithmetic with MCSAT
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
• Trace- and norm-compatible extensions of finite fields
• Pragmatic Quotient Types in Coq
• raSAT: An SMT Solver for Polynomial Constraints
• Zum Hilbertschen Nullstellensatz.
• Stacked garbling for disjunctive zero-knowledge proofs
• Computing and using minimal polynomials
• View of Computer Algebra Data from Coq
• Satisfiability modulo finite fields

Cited In (1)

• Satisfiability modulo finite fields

This page was built for publication: Satisfiability modulo finite fields

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