English

MACE 2.0 Reference Manual and Guide

Logic in Computer Science 2007-05-23 v1 Symbolic Computation
Authors: William McCune
View on arXiv ↗ PDF ↗

Abstract

MACE is a program that searches for finite models of first-order statements. The statement to be modeled is first translated to clauses, then to relational clauses; finally for the given domain size, the ground instances are constructed. A Davis-Putnam-Loveland-Logeman procedure decides the propositional problem, and any models found are translated to first-order models. MACE is a useful complement to the theorem prover Otter, with Otter searching for proofs and MACE looking for countermodels.

Keywords

first-order logic

Cite

@article{arxiv.cs/0106042,
  title  = {MACE 2.0 Reference Manual and Guide},
  author = {William McCune},
  journal= {arXiv preprint arXiv:cs/0106042},
  year   = {2007}
}

Comments

10 pages

Related papers

View all related →
Symbolic Computation · Computer Science
Mace4 Reference Manual and Guide
William McCune
2007-05-23
Artificial Intelligence · Computer Science
MACE: An Efficient Model-Agnostic Framework for Counterfactual Explanation
Wenzhuo Yang, Jia Li, Caiming Xiong, Steven C. H. Hoi
2022-06-01
Logic in Computer Science · Computer Science
Towards Practical First-Order Model Counting
Ananth K. Kidambi, Guramrit Singh, Paulius Dilkas, Kuldeep S. Meel
2025-06-11
Logic in Computer Science · Computer Science
Finding Finite Models in Multi-Sorted First Order Logic
Giles Reger, Martin Suda, Andrei Voronkov
2016-04-28
Computation and Language · Computer Science
A Multi-Agent Approach for Claim Verification from Tabular Data Documents
Rudra Ranajee Saha, Laks V. S. Lakshmanan, Raymond T. Ng
2026-04-21
Artificial Intelligence · Computer Science
PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic
Christoph Wernhard
2019-08-30
Logic in Computer Science · Computer Science
Computing Witnesses Using the SCAN Algorithm (Extended Preprint)
Fabian Achammer, Stefan Hetzl, Renate A. Schmidt
2025-06-03
Programming Languages · Computer Science
Alias and Change Calculi, Applied to Frame Inference
Alexander Kogtenkov, Bertrand Meyer, Sergey Velder
2013-07-12
Computation and Language · Computer Science
Iterated Decomposition: Improving Science Q&A by Supervising Reasoning Processes
Justin Reppert, Ben Rachbach, Charlie George, Luke Stebbing +3
2023-01-06
Machine Learning · Computer Science
Model Agnostic Contrastive Explanations for Structured Data
Amit Dhurandhar, Tejaswini Pedapati, Avinash Balakrishnan, Pin-Yu Chen +2
2019-06-04
General Relativity and Quantum Cosmology · Physics
Computer Algebra Solving of Second Order ODEs Using Symmetry Methods
E. S. Cheb-Terrab, L. G. S. Duarte, L. A. C. P. da Mota
2009-10-30
Computation and Language · Computer Science
A Relational Tsetlin Machine with Applications to Natural Language Understanding
Rupsa Saha, Ole-Christoffer Granmo, Vladimir I. Zadorozhny, Morten Goodwin
2021-02-23
Symbolic Computation · Computer Science
OTTER 3.3 Reference Manual
William McCune
2007-05-23
Combinatorics · Mathematics
A matrix approach to the structure, enumeration, and applications of partially ordered sets
Gi-Sang Cheon, Hong Joon Choi, Gukwon Kwon, Hojoon Lee +1
2026-02-05
Chemical Physics · Physics
Evaluation of the MACE Force Field Architecture: from Medicinal Chemistry to Materials Science
David Peter Kovacs, Ilyes Batatia, Eszter Sara Arany, Gabor Csanyi
2023-08-16
Artificial Intelligence · Computer Science
Bayesian Inference in Model-Based Machine Vision
Thomas O. Binford, Tod S. Levitt, Wallace B. Mann
2013-04-11
Logic in Computer Science · Computer Science
Computing Witnesses Using the SCAN Algorithm
Fabian Achammer, Stefan Hetzl, Renate A. Schmidt
2026-05-01
Logic in Computer Science · Computer Science
Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
Christoph Wernhard
2020-05-12
Programming Languages · Computer Science
Synthesis of models for order-sorted first-order theories using linear algebra and constraint solving
Salvador Lucas
2015-12-23
Machine Learning · Computer Science
Model Agnostic Supervised Local Explanations
Gregory Plumb, Denali Molitor, Ameet Talwalkar
2019-01-08
Logic in Computer Science · Computer Science
Verifying Relational Properties using Trace Logic
Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss +2
2019-08-13
Logic in Computer Science · Computer Science
Working with first-order proofs and provers
Michael Raskin, Christoph Welzel
2019-04-10
High Energy Physics - Phenomenology · Physics
A Proof of Concept for Matchete: An Automated Tool for Matching Effective Theories
Javier Fuentes-Martín, Matthias König, Julie Pagès, Anders Eller Thomsen +1
2023-07-31
Computation and Language · Computer Science
End-to-End Word-Level Pronunciation Assessment with MASK Pre-training
Yukang Liang, Kaitao Song, Shaoguang Mao, Huiqiang Jiang +5
2023-06-06
Logic in Computer Science · Computer Science
Detecting Unsolvable Queries for Definite Logic Programs
Maurice Bruynooghe, Henk Vandecasteele, D. Andre de Waal, Marc Denecker
2007-05-23