St Andrews Algorithm

• ...

• If outermost quantifier is existential

  • set variable to true and recurse

    • if result is success, succeed
    • if result is failure,

      • set the variable to false and recurse

• If outermost quantifier is universal

  • mark variable and recurse

    • if result is failure, fail
    • if result is success,

      • if current variable not involved in solution set, succeed
      • set the variable to false and recurse

• If only unmarked universal variables remain

  • return result of Davis Putnam on remaining clauses

Previous slide

Next slide

Back to first slide

View graphic version