Satisfiability modulo finite fields
From MaRDI portal
Publication:6535532
DOI10.1007/978-3-031-37703-7_8zbMATH Open1545.68086MaRDI QIDQ6535532
Gereon Kremer, Clark Barrett, Alex Ozdemir, Cesare Tinelli
Publication date: 12 January 2024
Finite fields (field-theoretic aspects) (12E20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A new method for solving algebraic systems of positive dimension
- Solving zero-dimensional algebraic systems
- Computation of Hilbert functions
- Trace- and norm-compatible extensions of finite fields
- A new efficient algorithm for computing Gröbner bases \((F_4)\)
- Efficient computation of zero-dimensional Gröbner bases by change of ordering
- The Magma algebra system. I: The user language
- On the theories of triangular sets
- Zum Hilbertschen Nullstellensatz.
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Stacked garbling for disjunctive zero-knowledge proofs
- Computing and using minimal polynomials
- SMT-based scenario verification for hybrid systems
- A mathematical introduction to logic.
- Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
- raSAT: An SMT Solver for Polynomial Constraints
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Solving Nonlinear Integer Arithmetic with MCSAT
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- The Lean Theorem Prover (System Description)
- Solving SAT and SAT Modulo Theories
- Secure Multiparty Computation Goes Live
- Probabilistic Algorithms in Finite Fields
- The knowledge complexity of interactive proof-systems
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- SINGULAR
- Cutting to the Chase Solving Linear Integer Arithmetic
- View of Computer Algebra Data from Coq
- Automated deduction for verification
- The MathSAT5 SMT Solver
- A Machine-Checked Proof of the Odd Order Theorem
- Pragmatic Quotient Types in Coq
- CoCoALib: A C++ Library for Computations in Commutative Algebra... and Beyond
- Computations in algebraic geometry with Macaulay 2
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- Satisfiability modulo finite fields
Related Items (1)
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)
