In First order Logic linear resolution is complete. So, either linear resolution finds the empty clause or it halts.
But what assures us that linear resolution halts in a finite number of iterations if the set of clauses is satisfiable ?
Asked
Active
Viewed 78 times
0
-
Possible duplicate of Linear Resolution Principle - First Order Logic – Mauro ALLEGRANZA Aug 28 '18 at 08:26
-
See also Completeness of Resolution Principles. – Mauro ALLEGRANZA Aug 28 '18 at 08:34