MACE4 and SEM: a comparison of finite model generators

DOI10.1007/978-3-642-36675-8_5zbMATH Open1383.68083OpenAlexW190372524MaRDI QIDQ4913862FDOQ4913862

Authors: Jian Zhang, Hantao Zhang 

Publication date: 16 April 2013

Published in: Automated Reasoning and Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-36675-8_5

Recommendations

• Towards Smarter MACE-style Model Finders
• scientific article; zbMATH DE number 1222426
• scientific article; zbMATH DE number 2219519
• Computing finite models by reduction to function-free clause logic
• Symmetry avoidance in MACE-style finite model finding

zbMATH Keywords

constraint propagationfinite modelsbacktracking search

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Constructing finite algebras with FALCON
• Title not available (Why is that?)
• Skew lattices in rings
• On the Foundations of Quasigroups
• Solution of the Robbins problem
• Implementing the Davis-Putnam method
• Automated model building
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Fast Decision Procedures Based on Congruence Closure
• The model evolution calculus.
• Existence of self-orthogonal diagonal Latin squares with a missing subsquare
• On middle distributivity for skew lattices
• Title not available (Why is that?)
• The structure of conjugacy closed loops
• Automated reasoning and exhaustive search: Quasigroup existence problems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Predicting and detecting symmetries in FOL finite model search
• Computing finite models by reduction to function-free clause logic
• A Powerful Technique to Eliminate Isomorphism in Finite Model Search
• Incomplete perfect Mendelsohn designs with block size four
• Existence of conjugate orthogonal diagonal Latin squares
• Note on a Lemma of Ladkin
• Title not available (Why is that?)
• Experiments with semantic paramodulation
• Title not available (Why is that?)
• The saga of the high school identities
• Self-orthogonal diagonal Latin square with missing subsquare
• Automated Deduction – CADE-20
• Artificial Intelligence and Symbolic Computation

Cited In (3)

• Blocking and other enhancements for bottom-up model generation methods
• Towards Smarter MACE-style Model Finders
• On First-Order Model-Based Reasoning

Uses Software

• MiniSat
• OTTER
• Darwin
• SATO
• SATCHMO
• SCOTT
• E-Darvin
• Mace4
• MGTP
• ModGen
• FALCON
• RRL

This page was built for publication: MACE4 and SEM: a comparison of finite model generators

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4913862)