Home Online Resources Table of Contents

Journal of Logic and Computation, Volume 8, Issue 4: August 1998.

A new method for automated finite model building exploiting failures and symmetries

N Peltier

Leibniz-Imag, 46, Avenue Félix Viallet, 38031 Grenoble Cedex, France

A method for building finite models is proposed. It combines enumeration of the set of interpretations on a finite domain with strategies in order to prune significantly the search space. The main new ideas underlying our method are to benefit from symmetries and from the information extracted from the structure of the problem and from failures of model verification tests. The algorithms formalizing the approach are given and the standard properties (termination, completeness, and soundness) are proven. The method can deal with first-order logic with equality. In contrast to existing ones, it does not require to transform the initial problem into a normal form and can be easily extended to other logics. Experimental results and comparisons with related works are reported.

Key words: Finite model building.

Pages 511-543


This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_08/Issue_04/080511.sgm.abs.html
Last modification: 11 September 1998.
Copyright© Oxford University Press, 1998.