MACE4 and SEM: a comparison of finite model generators

DOI10.1007/978-3-642-36675-8_5MaRDI QIDQ4913862zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

constraint propagationfinite modelsbacktracking search

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

Cites work

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

Cited in

(3)

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

Describes a project that uses

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)