MACE 2.0 Reference Manual and Guide

Simple item page
dc.creatorMcCune, William
dc.date2001-06-19
dc.date.accessioned2026-07-07T03:17:16Z
dc.date.available2026-07-07T03:17:16Z
dc.descriptionMACE 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.
dc.description10 pages
dc.identifierhttps://arxiv.org/abs/cs/0106042
dc.identifierhttp://arxiv.org/abs/cs/0106042
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/30659
dc.subjectLogic in Computer Science
dc.subjectSymbolic Computation
dc.subjectI.2.3; I.2.8
dc.titleMACE 2.0 Reference Manual and Guide
dc.typetext

Files

Collections

arXiv