|Page 338 of 800||Search internet|
Unary modus ponens expresses without specifying . Unary modus ponens , unary instantiation , and verification can be used for removing inferences operators , meta-quantifiers , and endorsements , 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 nor nor . 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.
|Page 338 of 800||Search logiweb.eu|