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

DOI10.1093/logcom/8.4.511zbMath0904.68155OpenAlexW2012294154MaRDI QIDQ4209295

Nicolas Peltier

Publication date: 11 January 1999

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/fa3ec031f0e20614d407cb24c864a2dd1280aa2b

zbMATH Keywords

finite models

Mathematics Subject Classification ID

Model theory of finite structures (03C13)

Related Items

Predicting and detecting symmetries in FOL finite model search ⋮ A calculus combining resolution and enumeration for building finite models ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ Constructing infinite models represented by tree automata ⋮ Automated Model Building: From Finite to Infinite Models

Uses Software

• SATCHMO
• SCOTT