Current Model Generation

• MACE 1.3.3
  • 150 second time limit per domain size search
  • Domain size = Number of constants
  • Domain size = 2 ... MACE
  • Top clause must be FALSE
    • Otherwise all extensions are pruned
    • Underlying idea is a search for contradiction
    • Typically the conjecture is the top clause
  • Take 1st model acceptable generated

• Why MACE?
  • Easy to use with TPTP (format module exists)
  • Algorithm easy to understand
  • Readable code

• Weaknesses of MACE
  • Cannot cope with large and complex problems
  • Can produce trivial models for Horn sets
    (Trivial models are typically ineffective)