8.5.13 Unary modus ponens

Prev Up Next Page 338 of 800 Search internet

Unary modus ponens A Ponens expresses A ponens B without specifying B. Unary modus ponens A Ponens, unary instantiation A At, and verification A Verify can be used for removing inferences operators C infer D, meta-quantifiers All x : C, and endorsements S endorse C, respectively, from the root of a term.

Adaption works by adding these three operators to argumentations as needed to make the argumentation fit the intended conclusion. Adaption is conservative in that it adds as few operators as possible to achieve its goal.

In some cases, adaption cannot adapt an argumentation to the intended conclusion. In such cases, you get an Cannot convert r to type t error where t can be 'infer', 'all', or 'endorse'.

In some situations, adaption has to adapt an argumentation to a conclusion where the conclusion has form neither C infer D nor All x : C nor S endorse C. In that case adaption just keeps adding unary modus ponens, unary instantiation, and verification operators until all inferences, meta-quantifiers, and endorsements in the root have been eliminated.

Prev Up Next Page 338 of 800 Search logiweb.eu

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