Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- articleMarch 2007
Polymorphic higher-order recursive path orderings
Journal of the ACM (JACM), Volume 54, Issue 1Article No.: 2, Pages 1–48https://doi.org/10.1145/1206035.1206037This article extends the termination proof techniques based on reduction orderings to a higher-order setting, by defining a family of recursive path orderings for terms of a typed lambda-calculus generated by a signature of polymorphic higher-order ...
- articleNovember 2006
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)
We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason ...
- articleNovember 1998
Ordered chaining calculi for first-order theories of transitive relations
We propose inference systems for binary relations that satisfy composition laws such as transitivity. Our inference mechanisms are based on standard techniques from term rewriting and represent a refinement of chaining methods as they are used in the ...
- articleSeptember 1997
Learning to reason
We introduce a new framework for the study of reasoning. The Learning (in order) to Reason approach developed here views learning as an integral part of the inference process, and suggests that learning and reasoning should be studied together.
The ...
-
- articleSeptember 1995
A theory of using history for equational systems with applications
Implementation of programming language interpreters, proving theorem of the form A=B, implementation of abstract data types, and program optimization are all problems that can be reduced to the problem of finding a normal form for an expression with ...
- articleJuly 1995
Logical foundations of object-oriented and frame-based languages
We propose a novel formalism, called Frame Logic (abbr., F-logic), that accounts in a clean and declarative fashion for most of the structural aspects of object-oriented and frame-based languages. These features include object identity, complex objects, ...
- articleMarch 1995
Decomposition of magic rewriting
The magic rewriting focuses on relevant data but suffers from additional rules, predicates, and tuples that are generated in search for the relevant data. Reducing the arity of predicates can cut down the number of such rules, predicates, and tuples by ...
- articleJanuary 1995
Reasoning about temporal relations: a maximal tractable subclass of Allen's interval algebra
We introduce a new subclass of Allen's interval algebra we call “ORD-Horn subclass,” which is a strict superset of the “pointisable subclass.” We prove that reasoning in the ORD-Horn subclass is a polynomial-time problem and show that the path-...
- articleNovember 1994
Modular stratification and magic sets for Datalog programs with negation
A class of “modularly stratified” logic programs is defined. Modular stratification generalizes stratification and local stratification, while allowing programs that are not expressible as stratified programs. For modularly stratified programs, the well-...
- articleNovember 1994
How to forget the past without repeating it
Bottom-up evaluation of deductive database programs has the advantage that it avoids repeated computations by storing all intermediate results and replacing recomputation by table lookup. However, in general, storing all intermediate results for the ...
- articleMarch 1994
Equational inference, canonical proofs, and proof orderings
We describe the application of proof orderings—a technique for reasoning about inference systems-to various rewrite-based theorem-proving methods, including refinements of the standard Knuth-Bendix completion procedure based on critical pair criteria; ...
- articleSeptember 1993
Modal nonmonotonic logics: ranges, characterization, computation
Many nonmonotonic formalism, including default logic, logic programming with stable models, and autoepistemic logic, can be represented faithfully by means of modal nonmonotonic logics in the family proposed by McDermott and Doyle. In this paper ...
- articleApril 1993
Automatic recognition of tractability in inference relations
A procedure is given for recognizing sets of inference rules that generate polynomial time decidable inference relations. The procedure can automatically recognize the tractability of the inference rules underlying congruence closure. The recognition of ...
- articleApril 1993
Taxonomic syntax for first order inference
A new polynomial time decidable fragment of first order logic is identified, and a general method for using polynomial time inference procedures in knowledge representation systems is presented. The results shown in this paper indicate that a ...
- articleApril 1992
Theorem proving using equational matings and rigid E-unification
In this paper, it is shown that the method of matings due to Andrews and Bibel can be extended to (first-order) languages with equality. A decidable version of E-unification called rigid E-unification is introduced, and it is shown that the method of ...