Name
Abstract | ||
|---|---|---|
A procedure is defined for deriving from any statement S an infinite sequence of statements S0, S1, S2, S3, ··· such that: (a) if there exists an i such that Si is unsatisfiable, then S is unsatisfiable; (b) if S is unsatisfiable, then there exists an i such that Si is unsatisfiable; (c) for all i the Herbrand universe of Si is finite; hence, for each i the satisfiability of Si is decidable. The new algorithms are then based on the idea of generating successive Si in the sequence and testing each Si for satisfiability. Each element in the class of new algorithms is complete. |
Year | DOI | Venue |
|---|---|---|
1974 | 10.1145/321812.321814 | Journal of the ACM (JACM) |
Keywords | DocType | Volume |
New Class,automated theorem-proving,Automated Theorem-Proving Algorithms,statements S0,Herbrand universe,new class,infinite sequence,successive Si,new algorithm,resolution,hyperresolution,automated theorem | Journal | 21 |
Issue | ISSN | Citations |
2 | 0004-5411 | 5 |
PageRank | References | Authors |
1.22 | 13 | 1 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ross A. Overbeek | 1 | 760 | 234.40 |