14.252 Ponens-seqop used on non-inference

Prev Up Next 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 << P ,, C ,, h infer x >> yields << P setunion {{ h }} ,, C ,, x >>. 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 h infer x. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 723 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05