3 ms·
Automated Propositional Sequent Proofs in the Browser with Tau Prolog
- chalst 6y agoThis 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.
- carapace 6y agoOne 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.)
- carapace 6y agoOh 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 https://en.wikipedia.org/wiki/Natural_deduction