Automating first-order relational logic

Abstract

An automatic analysis method for first-order logic with sets and relations is described. A first-order formula is translated to a quantifier-free boolean formula, which has a model when the original formula has a model within a given scope (that is, involving no more than some finite number of atoms). Because the satisfiable formulas that occur in practice tend to have small models, a small scope usually suffices and the analysis is efficient.

BibTeX

@inproceedings{Jackson:FSE00,
  author    = {Daniel Jackson},
  title     = {Automating first-order relational logic},
  booktitle = {FSE},
  pages     = {130--139},
  publisher = {{ACM}},
  year      = {2000},
}

Automating first-order relational logic

Abstract

Related papers