| |
 |
|
|
Henschen, Lawrence
Northwestern University
Evanston, Illinois
|
|
 |
|
|
| |
| |
|
Date Reviewed |
|
| |
1 - 7 of 7
reviews
|
|
|
|
|
|
|
|
The essence of logic
Kelly J., Prentice-Hall, Inc., Upper Saddle River, NJ, 1997. Type: Book (9780133963755)
Boolean and first-order logic, semantic methods and proof-based methods, and refutation methods are covered in this brief introduction to the basics of mathematical logic. Many of the chapters include examples taken from ordinary human...
|
Jun 1 1998 |
|
|
|
|
|
|
Horn functions and submodular Boolean functions
Ekin O., Hammer P. (ed), Peled U. Theoretical Computer Science 175(2): 257-270, 1997. Type: Article
Several results concerning subclasses of Horn Boolean formulas are presented. Theorem 1 states that a function f is Horn if and only if f ( x y ) <= f ( x ) ∨ f ( y ) for all
|
Dec 1 1997 |
|
|
|
|
|
|
Unification in commutative theories, Hilbert’s basis theorem, and Gröbner bases
Baader F. Journal of the ACM 40(3): 477-503, 1993. Type: Article
Unification in commutative theories is reduced to solving homogeneous linear equations in Z ⟨ X 1 ,..., X n ⟩. A series of algebraic theorems is presented, starting by establis...
|
Sep 1 1995 |
|
|
|
|
|
|
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 |
|
|
|
|
|
|
Introduction to HOL
Gordon M., Melham T. (ed), Cambridge University Press, New York, NY, 1993. Type: Book (9780521441896)
The authors start by providing a detailed description of the ML system for developing theorem proving programs. They then go on to the main topic of the book, the HOL theorem proving system, developed on top of ML. HOL is a reasoning s...
|
Aug 1 1994 |
|
|
|
|
|
|
Extended Horn sets in propositional logic
Chandru V., Hooker J. Journal of the ACM 38(1): 205-221, 1991. Type: Article
The intent of this research paper is to broaden the class of propositional formulas for which a linear-time decision procedure can be demonstrated. The authors define a new class of clause sets that has properties similar to sets of Ho...
|
Nov 1 1991 |
|
|
|
|
|
|
HOLMES: a deduction augmented database management system
Getta J., Rybiński H. Information Systems 9(2): 167-179, 1984. Type: Article
A front-end language for a deductive database management system is described. Only passing mention of the actual deductive techniques planned is made (in Section 4); this makes the title somewhat misleading. The language has two parts:...
|
Jun 1 1985 |
|
|
|
|
|
| |
|
|
| |
|
|
