Resource Limit Independence

The Effect of Resource Limits

• ATP systems can be (refutation) complete, but ...
  • They require inifinite resources
  • The search space is O(N ^2SearchDepth)
• Issues that affect (practical) completeness
  • Theory (calculus, search control)
  • Implementation
  • Resource limits (hardware, CPU time limit)

• Supply of resources is not under an ATP system's control

Peter Principle Points

• Looking at data from the TSTP
• Every system has a Peter Principle Point (PPP)
• Linear increase in resources past a PPP has little effect

System Performance Evaluation

• PPPs define "realistic resource limits"
• Provide sufficient resources for systems to reach PPPs
• And ask ... What Problems can they Solve?