Logiweb(TM)

14.270 Unchecked side condition

Prev Up Next Page 741 of 800 Search internet


Origin: check. Landing-place: diagnose.

In proof of d: Unchecked side condition: C

Users typically read proofs start to end and memorize what has been proved or assumed and thus can be used later in the proof. In contrast, the sequent evaluator evaluates proofs end to start and memorize which statements and side conditions have been used and thus have to be proved or assumed earlier in the proof. In a sequent << P ,, C ,, R >>, P is the set of statements that have to be proved or assumed earlier in the proof and C is the set of side conditions that have to be assumed earlier in the proof.

The 'Unchecked side condition' message indicates that the set C of side conditions was not empty after sequent evaluation. That may be because the side condition was used by modus probans in the proof but the side condition was not assumed in any, previous proof line. Another reason could be that the side condition was used by modus probans but should instead have been verified by the verify sequent operator which simply evaluates the side condition to see if it is true. The error may also indicate a bug in a tactic.

Prev Up Next Page 741 of 800 Search logiweb.eu

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