• PTTP and Linked Inference
• References
• Meson algorithm HOL light
• [Meson.ml(https://github.com/jrh13/hol-light/blob/master/meson.ml)
• This is used in HOL light's Meson.
• Model Elimination is a general proof method for first order logic.
• PTTP: implement model elimination using MESON technology.

§ Two groups of FOL solvers

• Bottom up and local: Resolution, inverse method (Maslov, Dok. Akad. Nauk '64).
• Top down and global: model elimination, tableaux.
• Both of these can be seen as proof search!
• Bottom up: start at assumptions, and derive more and more facts till we find the conclusion, or saturate.
• Top down: start at the conclusion, work backwards, break it down into subproblems till assumptions are reached.

§ Advantages of bottom up procedures

• Bottom up procedures compute proof at "meta level" (?) We can regard fvars as implicitly universally quantified (?)
• So it's possible to apply subsumption to the current set of facts (recall: subsumption lets us substitute to get more precise facts).
• In top down, fvars in different goals need to be correlated.
• However, top down is goal directed!
• they are much more economical to implement, since we only need to store the current subgoal.
• leanTAP: tableaux prover in five lines of prolog!