On Incremental Pre-processing for SMT

DOI10.1007/978-3-031-38499-8_3MaRDI QIDQ6492728zbMATH OpenFDO

Authors Nikolaj Bjørner, Katalin Fazekas

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_3

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• scientific article; zbMATH DE number 4037804 (Why is no real title available?)
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Transformation System for Developing Recursive Programs
• A unifying principle for clause elimination in first-order logic
• Blocked clause elimination for QBF
• Blocked clauses in first-order logic
• Clause elimination procedures for CNF formulas
• Computing small clause normal forms
• Efficiently solving quantified bit-vector formulas
• Exploiting symmetry in SMT problems
• Handbook of satisfiability. In 2 parts
• Hierarchical and Modular Reasoning in Complex Theories: The Case of Local Theory Extensions
• Horn clause solvers for program verification
• Incremental inprocessing in SAT solving
• Inprocessing rules
• New techniques for linear arithmetic: cubes and equalities
• On a generalization of extended resolution
• Optimized algorithms for incremental analysis of logic programs
• Precise and complete propagation based local search for satisfiability modulo theories
• Predicate Elimination for Preprocessing in First-Order Theorem Proving
• Preprocessing and Probing Techniques for Mixed Integer Programming Problems
• Preprocessing of propagation redundant clauses
• Presolve Reductions in Mixed Integer Programming
• Progress in presolving for mixed integer programming
• Reconstructing solutions after blocked clause elimination
• SAT-Inspired Eliminations for Superposition
• SAT-Inspired Higher-Order Eliminations
• Strong extension-free proof systems
• The strategy challenge in SMT solving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Two-row and two-column mixed-integer presolve using hashing-based pairing methods
• sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning

This page was built for publication: On Incremental Pre-processing for SMT

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