Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
MACE4 and SEM: A Comparison of Finite Model Generators
verfasst von : Hantao Zhang, Jian Zhang
Erschienen in: Automated Reasoning and Mathematics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This article has three objectives: (1) Promote Mace4, a program developed by Bill McCune that searches for finite models of first-order formulas and that is the best way to remember Bill. (2) Promote the research on model generation of first-order formulas. Mace4 remains one of the best model generation programs and we need newcomers who can take over Bill’s torch, because model generation is very important to automated reasoning and has many applications. (3) Compare Mace4 with SEM in detail so that the users of these tools or new model generator developers will understand the strengths and weaknesses of both systems and take advantage from this study.