Semantics, Solvability, and Decidability

Semantics

• Unbounded, infinite precision
• Standard interpretation of arithmetic
• Translation to FOF requires arithmetic type predicates

Solvability and Decidability

• ATP systems are expected to have varying abilities
  • Ground evaluation
  • ... (e.g., universally quantified formulae)
  • General arithmetic formulae
• I'm assured ...
  • Linear integer arithmetic (LIA) is decidable
  • Clausal LIA + uninterpreted predicates is semi-decidable
  • Clausal LIA + uninterpreted $int functions is undecidable
  • LIA + uninterpreted symbols undecidable
  • Integer arithmetic is undecidable