CADiZ

Reference manual / Z-related commands / Tactic application commands / Leibniz tac


The Leibniz tac built-in tactic is applicable to conjunction predicates. It performs Leibniz inferences, using any conjunct that is a schema predicate to rewrite all other occurrences of that predicate to true, and any conjunct that is a negated schema predicate to rewrite all other occurrences of that predicate to false. These results are then absorbed, and the tactic repeats until no further such rewriting is possible.

An approximation to this tactic is defined in section leibniztac. The differences are that the explicit definition suffers from loss of joker bindings, and it does not distinguish when no further rewriting is possible.

Tactic example

"apply tactic" p1 p2 "Leibniz tac"

This example applies the Leibniz tac built-in tactic to predicates p1 and p2.


IT 28-Dec-2005