Round 8: Tossup 18

Researchers at Cambridge and Munich developed the Isabelle system (10[1])for this task, which uses an HOL (10[1])approach that is based on the earlier LCF system created by Robert Milner. Setups for this task are often also used as solvers for SMT. (10[1])This task can be performed on well-formed recursively enumerable inputs using the DPLL algorithm. The outputs of this task are visualized by a semantic tableau, on which intermediate results (-5[1])are simplified using unification and resolution. (10[1]-5[1])The programming language ML was developed for this task, which is equivalent to functional programming by the Curry–Howard isomorphism. (10[1]-5[2])An “interactive” (-5[1])approach to this task (10[1])can be performed using Lean or Rocq. (10[3])For 10 (10[1])points, (10[1])1,834 reducible configurations (10[1])were checked by a computer to allow Appel and Haken to do what task (10[1])for the four-color theorem? (10[1])■END■ (10[4]0[2])

Back to tossups

Buzzes

Summary