A Model-Constructing Satisfiability Calculus
From MaRDI portal
Publication:2926635
DOI10.1007/978-3-642-35873-9_1zbMath1426.68251OpenAlexW70797468MaRDI QIDQ2926635
Dejan Jovanović, Leonardo de Moura
Publication date: 3 November 2014
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-35873-9_1
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Classical first-order logic (03B10) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Semantically-guided goal-sensitive reasoning: model representation, Interpolation and model checking for nonlinear arithmetic, Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, On First-Order Model-Based Reasoning, Modular strategic SMT solving with \textbf{SMT-RAT}, Propagation based local search for bit-precise reasoning, The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints, Local Search For Satisfiability Modulo Integer Arithmetic Theories, Unifying splitting, Levelwise construction of a single cylindrical algebraic cell, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test, Solving Nonlinear Integer Arithmetic with MCSAT, Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories, Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Conflict-driven satisfiability for theory combination: transition system and completeness, Deciding Bit-Vector Formulas with mcSAT, The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints, A unifying splitting framework, Editorial: Symbolic computation and satisfiability checking, From simplification to a partial theory solver for non-linear real polynomial constraints, A Survey of Satisfiability Modulo Theory, Wombit: a portfolio bit-vector solver using word-level propagation, Solving bitvectors with MCSAT: explanations from bits and pieces, SGGS decision procedures, Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description), Cutting to the chase., SAT-Inspired Eliminations for Superposition
Uses Software
