Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic

DOI10.1016/j.entcs.2008.04.077zbMath1277.68146OpenAlexW2020525563MaRDI QIDQ2864399

Ofer Strichman, Mirron Rozanov

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.04.077

zbMATH Keywords

equalities with uninterpreted functions

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Parallelizing SMT solving: lazy decomposition and conciliation

Uses Software

• SMT-LIB

Cites Work

• The small model property: How small can it be?
• Solvable cases of the decision problem
• Computer Aided Verification
• Computer Aided Verification
• Unnamed Item

This page was built for publication: Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic