Computing All Implied Equalities via SMT-Based Partition Refinement

DOI10.1007/978-3-319-08587-6_12MaRDI QIDQ3192188zbMATH OpenOpenAlexFDO

Authors Josh Berdine, Nikolaj Bjørner

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08587-6_12

zbMATH Keywords

satisfiability modulo theoriesdecision proceduressoftware verificationcongruence closureconsequence findingimplied equalities

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mechanization of proofs and logical operations (03B35)

Recommendations

• Using SMT for solving fragments of parameterised Boolean equation systems
• Generalizing DPLL and satisfiability for equalities
• Equality reasoning in sequent-based calculi
• scientific article; zbMATH DE number 1552532
• scientific article; zbMATH DE number 3898849
• SMELS: Satisfiability Modulo Equality with Lazy Superposition
• SMELS: satisfiability modulo equality with lazy superposition
• A theory of complete logic programs with equality
• An algorithm for the class of pure implicational formulas

Cited in

(2)

• Quantitative abstractions for collective adaptive systems
• Symbolic computation of differential equivalences

This page was built for publication: Computing All Implied Equalities via SMT-Based Partition Refinement

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