Predicting and detecting symmetries in FOL finite model search

DOI10.1007/s10817-006-9040-3zbMath1107.68092OpenAlexW2073006675MaRDI QIDQ861703

Laurent Henocque, Belaïd Benhamou, Gilles Audemard

Publication date: 30 January 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-006-9040-3

zbMATH Keywords

extended least number heuristicleast number heuristic

Mathematics Subject Classification ID

Related Items (3)

MACE4 and SEM: A Comparison of Finite Model Generators ⋮ Boosting isomorphic model filtering with invariants ⋮ Constructing infinite models represented by tree automata

Uses Software

• nauty
• TPTP
• FINDER
• Mace4
• FALCON

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The TPTP problem library. CNF release v1. 2. 1
• Tractability through symmetries in propositional calculus
• Constructing finite algebras with FALCON
• Networks of constraints: Fundamental properties and applications to picture processing
• Automatic Detection of Variable and Value Symmetries
• A new method for automated finite model building exploiting failures and symmetries
• Decision procedures and model building in equational clause logic

This page was built for publication: Predicting and detecting symmetries in FOL finite model search