Computing All Implied Equalities via SMT-Based Partition Refinement

DOI10.1007/978-3-319-08587-6_12zbMATH Open1423.68408OpenAlexW97129115MaRDI QIDQ3192188FDOQ3192188

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

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

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)

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)