Automated Propositional Sequent Proofs in the Browser with Tau Prolog | Hacker News Reader

Automated Propositional Sequent Proofs in the Browser with Tau Prolog

philipzucker.com

33 pointsphilzook3 comments

This is a nice introduction to proof search.

A clarification: a rule is invertible if when the conclusion is provable, each of the premises is. The most important example of a non-invertible rule is weakening:

     Gamma    |- Delta       Gamma |- Delta
     -----------------       -----------------
     Gamma, A |- Delta       Gamma |- Delta, A

The point about applying invertible rules eagerly is why proof systems designed for proof search are formulated so that most of the rules are invertible, and use of non-invertible rules can be pushed up the deduction as far as possible: in the case of weakening, the rule can be pushed so it appears before all others.

One interesting thing to do here would be to reorder the clauses of the Prolog predicate to see the effect on the size of the proof. Or write a meta-interpreter to automatically try searching over permutations of the rules, or with a cost parameter... (I'd better stop now or I won't get anything done today.)

Oh very, very nice!

Otten has more efficient solvers in "Part 3: Tableau and Connection Provers" but i find the sequent proofs much easier to understand (which makes sense, the "natural" in "Natural Deduction" means something like "intuitive" as used in IT.)

https://en.wikipedia.org/wiki/Natural_deduction

Reply on news.ycombinator.com