On Variable-inactivity and Polynomial Formula-Satisfiability Procedures

DOI10.1093/logcom/exm055zbMath1144.03007OpenAlexW2113890674WikidataQ118123663 ScholiaQ118123663MaRDI QIDQ5450569

Maria Paola Bonacina, Mnacho Echenim

Publication date: 12 March 2008

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exm055

zbMATH Keywords

satisfiability modulo theoriesdecision procedurestheory reasoningrewrite-based theorem-provingtheories of data structures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Interpolation systems for ground proofs in automated deduction: a survey, Modular Termination and Combinability for Superposition Modulo Counter Arithmetic, On deciding satisfiability by theorem proving with speculative inferences, An instantiation scheme for satisfiability modulo theories, Canonical Ground Horn Theories, On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving, Variant-Based Satisfiability in Initial Algebras, Satisfiability Procedures for Combination of Theories Sharing Integer Offsets, Data Structures with Arithmetic Constraints: A Non-disjoint Combination, Theory decision by decomposition, On interpolation in automated theorem proving