Satisfiability modulo finite fields

DOI10.1007/978-3-031-37703-7_8MaRDI QIDQ6535532zbMATHFDO

Authors Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark Barrett

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)

Recommendations

• Computer Aided Verification
• Satisfiability modulo linear arithmetic over a finite ring
• A survey of satisfiability modulo theory
• Satisfiability modulo theories

Cites work

• scientific article; zbMATH DE number 417578 (Why is no real title available?)
• scientific article; zbMATH DE number 4083539 (Why is no real title available?)
• scientific article; zbMATH DE number 1305433 (Why is no real title available?)
• scientific article; zbMATH DE number 1970438 (Why is no real title available?)
• scientific article; zbMATH DE number 2151220 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• scientific article; zbMATH DE number 274299 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• A machine-checked proof of the odd order theorem
• A mathematical introduction to logic.
• A model-constructing satisfiability calculus
• A new efficient algorithm for computing Gröbner bases \((F_4)\)
• A new method for solving algebraic systems of positive dimension
• Automated deduction for verification
• CoCoALib: A C++ library for computations in commutative algebra\(\dots \) and beyond
• Computation of Hilbert functions
• Computations in algebraic geometry with Macaulay 2
• Computing and using minimal polynomials
• Cutting to the chase. Solving linear integer arithmetic
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Efficient computation of zero-dimensional Gröbner bases by change of ordering
• Formalizing Some “Small” Finite Models of Projective Geometry in Coq
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• On the theories of triangular sets
• Polyhedral approximation of multivariate polynomials using Handelman's theorem
• Pragmatic quotient types in Coq
• Probabilistic Algorithms in Finite Fields
• Quantifier elimination for real algebra -- the quadratic case and beyond
• SINGULAR
• SMT-based scenario verification for hybrid systems
• Satisfiability modulo finite fields
• Secure multiparty computation goes live
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving non-linear arithmetic
• Solving nonlinear integer arithmetic with MCSAT
• Solving zero-dimensional algebraic systems
• Stacked garbling for disjunctive zero-knowledge proofs
• The Lean theorem prover (system description)
• The Magma algebra system. I: The user language
• The MathSAT5 SMT solver
• The knowledge complexity of interactive proof-systems
• Trace- and norm-compatible extensions of finite fields
• View of computer algebra data from Coq
• Zum Hilbertschen Nullstellensatz.
• \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
• raSAT: An SMT Solver for Polynomial Constraints

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)