Automating first-order relational logic

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. The paper presents a simple logic and gives a compositional translation scheme. It also reports briefly on experience using the Alloy Analyzer, a tool that implements the scheme. Keywords First-order logic; relational logic; Z specification; object models; automatic analysis; model finding; constraint solvers; SAT solvers.

• Type: Conference
• Year: 2000
• Where: SIGSOFT
• Authors: Daniel Jackson
• Keywords: Automatic Analysis, First-order Logic, Quantifier-free Boolean Formula, SIGSOFT 2000, Software Engineering