Matching not implemented for every proved law with THERE EXISTS and FOR ALL involved about qed HOT 4 CLOSED

Yes, as mentioned in Ex 14.1, most exercises from this point onwards do not have matching implemented (more precisely, any law involving a predicate, operator, or term does not have matching implemented unless there is a specific hardcoded matching routine for that law). Any specific law can be matched by a custom matching algorithm, but this takes a certain amount of time (particularly with regards to debugging) and about a page worth of code. Ideally there should be a general solution that does not require individual matching algorithms for each exercise; I don't have a good proposal for this currently, particularly for those laws where the matching is non-unique.

from qed.

Actually, it occurs to me that for some of these exercises, one can use the existing matching method for a simpler template (replacing some predicate terms with atomic propositions). For instance, Ex 22.6(b) (from FOR ALL X: THERE EXISTS Y: Q(X,Y), deduce THERE EXISTS Y: FOR ALL X: Q(X,Y)) can be matched using the template FOR ALL X: THERE EXISTS Y: A, deduce THERE EXISTS Y: FOR ALL X: A because no substitution actually occurs within the Q(X,Y) term, and also the side conditions of what variables are allowed to be used in Q(X,Y) or in A are the same. So I could code a proxy template for several of these laws which would reduce the number of laws without matching capability, though it would not eliminate them entirely. (But then again many of the later laws are unlikely to be useful in matching anyway, for instance it's unlikely that the Lewis Carroll syllogism will see much use.)

In the meantime, I have placed an explicit notice in the notes for every exercise for which matching is not currently implemented.

from qed.

from qed.

OK, I've managed to use such proxy templates to implement matching for a large number of exercises that previously could not be matched (For instance, all of the syllogisms now can be used for matching). There are still a number of exercises which are not matchable at present, but the issue seems to be significantly less serious now.

from qed.