|Page 723 of 800||Search internet|
Origin: check. Landing-place: diagnose.
Ponens-seqop used on non-inference R
The Ponens sequent operator applied to a sequent yields . Thus, the Ponens operator allows to move a hypothesis h from the conclusion to the set of premisses. Meta-modus-ponens can be implemented as a Cut sequent operator whose second argument has a Ponens sequent operator as principal operator.
The 'Ponens-seqop used on non-inference' indicates that the conclusion of the sequent did not have form . The error may indicate an error in the proof or a bug in a tactic.
|Page 723 of 800||Search logiweb.eu|