| |
Browse All Reviews > Computing Methodologies (I) > Artificial Intelligence (I.2) > Deduction And Theorem Proving (I.2.3) > Resolution (I.2.3...)
|
|
 |
|
|
| |
|
|
| |
1-8 of 8
Reviews about "Resolution (I.2.3...)":
|
Date Reviewed |
| |
An answer to an open problem of Urquhart
Egly U. Theoretical Computer Science 198(1-2): 201-209, 1998. Type: Article
Egly answers a question raised by Urquhart in a 1995 paper [1], where he proves that resolution with limited extension (Rle), a Gentzen system G based on the biconditional ( as the only connective, and G extended by the analytic cut ru...
|
Dec 1 1998 |
| |
Resolution proof systems
Stachniak Z., Kluwer Academic Publishers, Norwell, MA, 1996. Type: Book (9780792340171)
This monograph is an attempt to investigate logical systems and their resolution proof systems using a unified abstract algebra–based framework. The book deals with automated reasoning programs in the context of nonclassical ...
|
Oct 1 1997 |
| |
A resolution principle for constrained logics
Bürckert H. Artificial Intelligence 66(2): 235-271, 1994. Type: Article
Bürckert extends and unifies various theories about constrained quantifiers (such as sorted resolution, theory unification, and theory resolution) as applied to resolution theorem proving. The idea is to al...
|
Jun 1 1995 |
| |
A theory of conflict resolution in planning
Yang Q. Artificial Intelligence 58(1-3): 361-392, 1992. Type: Article
A theory of conflict resolution in AI planning is presented. The paper proposes a strategy for handling conflicts in a global manner, using constraint satisfaction techniques. It shows that this strategy can reduce the search space. Ya...
|
Dec 1 1993 |
| |
First-order logic and automated theorem proving
Fitting M., Gries D., Springer-Verlag New York, Inc., New York, NY, 1990. Type: Book (9780387972336)
In the authors’ words, this book is intended for computer scientists interested in automated theorem proving in classical logic. It contains a thorough presentation of formal logic and many proof techniques. This treatment of...
|
Apr 1 1991 |
| |
On determining the causes of nonunifiability
Cox P. Journal of Logic Programming 4(1): 33-58, 1987. Type: Article
A pair of expressions e1 and e2 (called a constraint) is unifiable when e1 and e2 can be made identical by uniformly substituting the variables in th...
|
Jun 1 1988 |
| |
Unification in datastructure multisets
Büttner W. Journal of Automated Reasoning 2(1): 75-88, 1986. Type: Article
An essential part of the resolution method widely used in artificial intelligence (e.g., in Prolog) is unification of terms ti, i.e., finding a substitution s for which s(t1) = S...
|
Jul 1 1987 |
| |
Completeness results for inequality provers
Bledsoe W., Kunen K., Shostak R. Artificial Intelligence 27(3): 255-288, 1985. Type: Article
This paper provides the theoretical formalism for the automated deduction system developed by Bledsoe and Hines [1] which uses a variation of resolution to discover proofs about dense total orders without endpoints. In particular, the ...
|
Mar 1 1987 |
| |
|
|
| |
|
|
