Abstract
Finite model search for first-order logic theories is complementary to theorem proving. Systems like Falcon, SEM and FMSET use the known LNH (Least Number Heuristic) heuristic to eliminate some trivial symmetries. Such symmetries are worthy, but their exploitation is limited to the first levels of the model search tree, since they disappear as soon as the first cells have been interpreted. The symmetry property is well-studied in propositional logic and CSPs, but only few trivial results on this are known on model generation in first-order logic.
We study in this paper both an ordering strategy that selects the next terms to be interpreted and a more general notion of symmetry for finite model search in first-order logic. We give an efficient detection method for such symmetry and show its combination with the trivial one used by LNH and LNHO heuristics. This increases the efficiency of finite model search generation. The method SEM with and without both the function ordering and symmetry detection is experimented on several interesting mathematical problems to show the advantage of reasoning by symmetry and the function ordering.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
G. Audemard and L. Henocque. The extended least number heuristic. Proceedings of the first International Joint Conference in Automated Reasoning (IJCAR), Springer Verlag, 2001.
B. Benhamou and L. Henocque. A hybrid method for finite model search in equational theories. Fundamenta Informaticae, 39(1–2):21–38, 1999.
B. Benhamou and L. Sais. Tractability through symmetries in propositional calculus. Journal of Automated Reasoning, 12(1):89–102, 1994.
J. Crawford. A theorical analisys of reasoning by symmetry in first-order logic. In Proceedings of Workshop on Tractable Reasonning, AAI92, pages 17–22, 1992.
J. Crawford, M. L. Ginsberg, E. Luck, and A. Roy. Symmetry-breaking predicates for search problems. In proceedings of KR’96, pages 148–159. 1996.
M. Fujita, J. Slaney, and F. Bennett. Automatic generation of some results in finite algebra. In Proceedings of International Joint Conference on Artificial Intelligence, pages 52–57. Morgan Kaufmann, 1993.
N. Peltier. A new method for automated finite model building exploiting failures and symmetries. Journal of Logic and Computation, 8(4):511–543, 1998.
C. Suttner and G. Sutcliffe. The TPTP Problem Library. Technical Report, J. Cook University, 1997. http://www.cs.jcu.edu.au/ftp/pub/techreports/97-8.ps.gz
J. Zhang. Problems on the Generation of Finite Models. In proceedings of the 12th International Conference on Automated Deduction, LNAI 814, pages 753–757, Nancy, France, 1994. Springer-Verlag.
J. Zhang. Constructing finite algebras with FALCON. Journal of Automated Reasoning, 17(1):1–22, August 1996.
J. Zhang. Test Problems and Perl Script for Finite Model Searching. Association of Automated Reasoning, Newsletter 47, 2000. http://www-unix.mcs.anl.gov/AAR/issueapril00/issueapril00.html
J. Zhang and Hantao Zhang. SEM: a system for enumerating models. In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, pages 298–303, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Audemard, G., Benhamou, B. (2002). Reasoning by Symmetry and Function Ordering in Finite Model Generation. In: Voronkov, A. (eds) Automated Deduction—CADE-18. CADE 2002. Lecture Notes in Computer Science(), vol 2392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45620-1_19
Download citation
DOI: https://doi.org/10.1007/3-540-45620-1_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43931-8
Online ISBN: 978-3-540-45620-9
eBook Packages: Springer Book Archive