The Small Model Property: How Small Can It Be?

Efficient decision procedures for equality logic (quantifier-free predicate calculus+the equality sign) are of major importance when proving logical equivalence between systems. We introduce an efficient decision procedure for the theory of equality based on finite instantiations. The main idea is t...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2002-10, Vol.178 (1), p.279-293
Main Authors: Pnueli, Amir, Rodeh, Yoav, Strichman, Ofer, Siegel, Michael
Format: Article
Language:English
Subjects:
Exact sciences and technology
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Recursion theory
Sciences and techniques of general use
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Efficient decision procedures for equality logic (quantifier-free predicate calculus+the equality sign) are of major importance when proving logical equivalence between systems. We introduce an efficient decision procedure for the theory of equality based on finite instantiations. The main idea is to analyze the structure of the formula and compute accordingly a small domain to each variable such that the formula is satisfiable iff it can be satisfied over these domains. We show how the problem of finding these small domains can be reduced to an interesting graph theoretic problem. This method enabled us to verify formulas containing hundreds of integer and floating point variables that could not be efficiently handled with previously known techniques.
ISSN:0890-5401
1090-2651
DOI:10.1006/inco.2002.3175