Building small equality graphs for deciding equality logic with uninterpreted functions

DOI10.1016/J.IC.2005.08.001MaRDI QIDQ2490118zbMATH OpenOpenAlexFDO

Authors Yoav Rodeh, Ofer Strichman

Publication date 28 April 2006

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2005.08.001

zbMATH Keywords

decidabilitypositive equality

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Decidability and field theory (12L05) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• LATIN 2004: Theoretical Informatics
• BDD based procedures for a theory of equality with uninterpreted functions
• scientific article; zbMATH DE number 1796130
• scientific article; zbMATH DE number 2081115
• scientific article; zbMATH DE number 2102727

Cites work

• BDD based procedures for a theory of equality with uninterpreted functions
• Computer Aided Verification
• Computer Aided Verification
• scientific article; zbMATH DE number 1670770 (Why is no real title available?)
• scientific article; zbMATH DE number 2081115 (Why is no real title available?)
• scientific article; zbMATH DE number 1796130 (Why is no real title available?)
• scientific article; zbMATH DE number 1798182 (Why is no real title available?)
• scientific article; zbMATH DE number 1798183 (Why is no real title available?)
• scientific article; zbMATH DE number 1903346 (Why is no real title available?)
• scientific article; zbMATH DE number 1903374 (Why is no real title available?)
• scientific article; zbMATH DE number 2090300 (Why is no real title available?)
• scientific article; zbMATH DE number 2102726 (Why is no real title available?)
• scientific article; zbMATH DE number 2102727 (Why is no real title available?)
• Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
• Solvable cases of the decision problem
• The code validation tool (CVT). Automatic verification of a compilation process
• The small model property: How small can it be?
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(12)

• The small model property: How small can it be?
• BDD based procedures for a theory of equality with uninterpreted functions
• General lower bounds and improved algorithms for infinite-domain CSPs
• Reduced functional consistency of uninterpreted functions
• scientific article; zbMATH DE number 2081115 (Why is no real title available?)
• scientific article; zbMATH DE number 1796130 (Why is no real title available?)
• scientific article; zbMATH DE number 1798182 (Why is no real title available?)
• scientific article; zbMATH DE number 2102726 (Why is no real title available?)
• scientific article; zbMATH DE number 2102727 (Why is no real title available?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Technology for Verification and Analysis
• LATIN 2004: Theoretical Informatics

Describes a project that uses

Uses Software

• CVT
• UCLID
• CVC
• EVC
• ICS

This page was built for publication: Building small equality graphs for deciding equality logic with uninterpreted functions

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