Rövid szöveges bemutatás:
A lineáris rezolúció a rezolúció egy speciális fajtája. A rezolúciós eljárásban rezolvensek keletkeznek, azaz olyan elem amely egy rezolúciós összevonási lépésnek az eredménye. A lineáris rezolúció abban köti meg a teljes folyamatot, hogy a keletkezett rezolvenst a következő bizonyítási ciklusban fel kell használnunk mint klóz. Tehát az első keletkezett rezolvenst, a következő rezolúciós összevonásnál fel kell használni, és mellé egy másik állítást, mely kettőből új rezolvenst kapunk. Ezt addig ismételjük, míg meg nem kapjuk az üres klózt. Ha az üres klóz valamilyen módszerrel előállítható, akkor a lineáris rezolúcióval is előállítható.