3 ms·
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 import
by chalst 6y ago
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.
- 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.)