AUTOMATED THEOREM PROVING
45
Resolution Creators· Importance
Retlnement
(Appro:~:.
Date]
1. Basic resolution
I.A.
Robinson Oriainal resolution
[1984] proof procedure
2.
Unit preference
Wos,G. Robinson, Used in AURA
Canon [1984]
3. Set-of-support Wos,G. Robinson, Used in AURA and
Carson [1984] ITP
4.
Hyperresolution
I.A.
Robinson Used in AURA and
[1985] ITP
5.
Model elimination Loveland
Completion or problem
[1985] reduction format: Basis for
Slrresolution
8. Linear resolution
Loveland Implements depth-drst
Luckham [1988] search in resolution
7. SL-resolution Kowalski Very tJahtly constrained
Kuehner [1970]
linear resolution: Used
(Toes
resolution)
{Loveland) in early version of
PROLOG lanauqe
a.
Locking Boyer
V~ry
t.iahtly constrained
[1970] ordered-clause resolution
/n.com.plete
~nem.ents
9. Unit clause Wos et al. · These forms are
resolution [1984] complete for Hom
Input clause
Cbang,others
clause logic:
resolution
[1970]
Input resolution is the
underlying format in the
present PROLOG language
Jlmfttll.*'tl
SfWII"'v
10. Paramodulation Wos,G. Robinson
Eliminates the need for
{Demodulation)
( +
Carson. Shalla) almost all
[1988] ([1987])
equalit:y uio11111
Some resolution variants and related procedures
I'IG1JJIB 8
Previous Page Next Page