TERMIUM Plus^®

Fiche 1,  Justifications,  Anglais

Record number: 1, Textual support number: 1 CONT

Linear resolution (also called ancestry-filtered resolution) is a slight generalization of input resolution. A linear resolvent is one in which at least one of the parents is either in the initial database or is an ancestor of the other parent. A linear deduction is one in which each derived clause is a linear resolvent. A linear refutation is a linear deduction of the empty clause (). Linear resolution takes its name from the linear shape of the proofs it generates. A linear deduction starts with a clause in the initial database (called the top clause) and produces a linear chain of resolutions.  1, fiche 1, Anglais, - ancestry%2Dfiltered%20resolution

Fiche 1,  Justifications,  Français

Fiche 1,  Justifications,  Espagnol