Information and Computation 162 1/2 (2000) 3-23, (with Paliath Narendran and Qing Guo).
We consider the complexity of equational unification and matching problems where the equational theory contains a nilpotent function, i.e., a function f satisfying f(x,x) = 0 where 0 is a constant. We show that nilpotent unification and matching are NP-complete. In the presence of associativity and commutativity, the problems still remain NP-complete. However, when 0 is also assumed to be the unity for the function f, the problems are solvable in polynomial time. We also show that the problem remains in P even when a homomorphism is added. An application of this result to a subclass of set-constraints is illustrated. Second-order matching modulo nilpotence is shown to be undecidable.
© 2000 by Academic Press.
Journal of Symbolic Computation 29, 1 (2000) 79-82.
We give a formula for the general solution of a d-th order linear difference equation with constant coefficients in terms of one of the solutions of its associated homogeneous equation. The formula neither uses the roots of the characteristic equation nor their multiplicities. It can be readily generalised to the case where the domain of the difference equation is the real numbers, and the initial values are given by a function defined on the interval [0, d). In both cases, we express the general solution of the difference equation in terms of a single solution of its associated homogeneous equation at integer arguments.
© 2000 by Academic Press.
CADE system descriptions do not have abstracts.
The Fibonacci Quarterly 36.2 (May 1998): 129-45.
Supplementary abstract: papers in The Fibonacci Quarterly do not have abstracts.
We derive continuous solutions of generalizations of Fibonacci recurrences where at least two predecessors are summed. These recurrences may either have arbitrary initial values, or an initial function. We give properties of the characteristic equation of these recurrences including its discriminant, location of roots, reducibility, and solvability in radicals. We also present a series for the positive real root of the characteristic equation. We then present a general formula for the solution of homogeneous linear difference equations whose characteristic equations have simple roots. This enables a Binet formula for the generalized recurrences to be directly derived. We show that this formula subsumes three previous generalizations of Fibonacci's sequence. We also discuss our alternative method of solution which uses the Laplace Transform.
Automated Deduction - CADE-13: Thirteenth International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 1104 (Springer, Berlin, 1996) 261-274. (With Paliath Narendran and Qing Guo).
We consider equational unification and matching problems where the equational theory contains a nilpotent function, i.e., a function f satisfying f(x,x) = 0 where 0 is a constant. Nilpotent matching and unification are shown to be NP-complete. In the presence of associativity and commutativity, the problems still remain NP-complete. But when 0 is also assumed to be the unity for the function f, the problems are solvable in polynomial time. We also show that the problem remains in P even when a homomorphism is added. Second-order matching modulo nilpotence is shown to be undecidable.
© 1996 by Springer-Verlag.
Artificial Intelligence in Medicine 7 (1995) 93-116.
INTERNIST-I was an expert system designed in the early 1970's to diagnose multiple diseases in internal medicine by modelling the behaviour of clinicians. Its form and operation are described, and evaluations of the system are surveyed. The major result of the project was its knowledge base which has been used in successor systems for medical education and clinical use. We also survey the effects of the project through these systems, and conclude that the most successful of them in the near future is likely to be Quick Medical Reference (QMR) when used as an ``electronic textbook'' of medicine.
© 1995 Elsevier Science B.V.
Theoretical Computer Science, 136, 1, (1994) 277-289.
We give a model-theoretic semantics for the logic of higher-order Horn clauses, the basis of a form of the lambda-Prolog higher-order logic programming language. We define certain intensional general models and show that higher-order Horn clause logic is sound and complete with respect to them.
© 1994 - Elsevier Science B.V.
TYPES '93, Selected Papers, Lecture Notes in Computer Science 806 (Springer, Berlin, 1994) 366-383.
We give declarative and operational semantics for logics that are expressible as finite sets of abstract clauses. The declarative semantics for these sets of generalized Horn clauses uses inductively defined sets and fixed points. It is shown to coincide with the operational semantics for successful and finitely failed derivations. The Abstract Clause Engine (ACE) implements proofs with abstract clauses. The semantics given here provide criteria for ACE's correctness and completeness.
© 1993 by Springer-Verlag.
Object-Based Concurrent Computing, Lecture Notes in Computer Science 612 (Springer, Berlin, 1992) 81-98. European Conference on Object-Oriented Programming (ECOOP '91) Workshop, Geneva, Switzerland, July 1991. (With Joseph Goguen)
We present a sheaf semantics for concurrent method expression evaluation in FOOPS. Evaluations of functions, methods, and attributes are treated in a uniform way. General E-strategies for functions, methods, attributes, and method combiners are assumed.
© 1992 by Springer-Verlag.
In Robert Meersman, William Kent and Samit Khosla, (editors), Object Oriented Databases: Analysis, Design & Construction,(North-Holland, Amsterdam, 1991) 1-22. (With Joseph Goguen). Proceedings of the Fourth IFIP TC-2 Working Conference on Data Semantics (DS-4).
In describing object oriented systems, the word ``type'' is used for at least three different levels: data, objects, and modules. In FOOPS, these three are carefully distinguished both syntactically and semantically, and given a rigorous algebraic semantics. Order sorted algebra is used for the semantics of data and of objects; the semantics of objects also uses hidden sorts, and the semantics of modules is based on theories. This paper describes this three-fold approach to types and compares it with aspects of some other approaches, including type theoretic approaches and the language Eiffel. We conclude that failure to distinguish among the different types of ``type'' can lead to unnecessary complication and limitation.
© 1991 by North-Holland.
Rewriting Techniques and Applications, Fourth International Conference, RTA-91, Lecture Notes in Computer Science 488 (Springer, Berlin, 1991) 25-36.
We give here a general definition of term rewriting in the simply typed lambda-calculus, and use it to define higher-order forms of term rewriting systems, and equational unification and their properties. This provides a basis for generalizing the first- and restricted higher-order results for these concepts. As examples, we generalize Plotkin's criteria for building-in equational theories, and show that pure third-order equational matching is undecidable. This approach simplifies computations in applications involving lexical scoping, and equations. We discuss open problems and summarize future research directions.
© 1991 by Springer-Verlag.
Proceedings of the Tenth International Conference on Automated Deduction (CADE-10), Lecture Notes in Artificial Intelligence 449 (Springer, Berlin, 1990) 679-680.
Supplementary abstract: CADE system descriptions do not have abstracts.
The Abstract Clause Engine (ACE) solves problems defined by abstract clauses such as classical combinatorial search problems, logic programming searches, and sequent calculus proofs. The user need only supply the grammar of the input problem, a consistency test, and example problems. The user can select and measure the performance of a variety of search methods such as backtracking, and generalisations of forward checking and depth-first iterative deepening. Its generic approach enables prototype systems to be constructed and compared easily. ACE is written in Standard ML and makes use of its polymorphism and modules.
Journal of Automated Reasoning, 5:37-47, 1989.
Restrictions of the problem of finding all maximal unifiable or minimal nonunifiable subsets to those of certain sizes are shown to be NP-hard, and consequently inappropriate in general for reducing thrashing by intelligent backtracking in resolution theorem provers and logic program executions. We also show that existing backtrack methods based on the computation of all maximal unifiable subsets of assignments as a means to avoid thrashing are intractable because the solution length of these subsets can increase exponentially with the input length, and we give a corresponding result for minimal nonunifiability. The results apply not only to standard unification, but to a characterized collection of unification algorithms which includes unification without the occurs check. This now justifies the necessity for approximate or heuristic approaches to reduce thrashing in resolution theorem provers and the execution of logic programs.
© 1989 by Kluwer Academic Publishers.
Information Processing Letters, 32:85-87, 1989.
Supplementary abstract: papers in Information Processing Letters do not have abstracts.
We introduce two optimisations of forward checking (FC): partial filtering which applies when search rearrangement (SR) is used, and partial stacking. The former reduces the number of consistency tests required to solve a consistent labelling problem such as the eight queens problem, or a logic programming search. Partial stacking reduces memory requirements. Empirical results are given for partial filtering. We also show that FC has exponential overheads in general. Adding a form of intelligent backtracking to FC+SR cannot change decision points and can only make FC+SR slower.
Third International Conference on Logic Programming, Lecture Notes in Computer Science 225 (Springer, Berlin, 1986) 107-121.
Intelligent backtracking in logic programs analyses unification failure to avoid thrashing, which is an inefficient behaviour of ordinary backtracking. We show that the computation of all maximal unifiable subsets of constraints, as a means to avoid thrashing, is intractable in the sense that the solution length can be non-polynomially related to the input length. We also give a corresponding result for minimal nonunifiability. Restrictions of the problem of finding all maximal unifiable (minimal nonunifiable) subsets to those of certain sizes, for use with heuristics, are shown to be NP-hard. The reults apply not only to standard unification but for unification without the occur-check as in many versions of Prolog. This now justifies the necessity for approximate or heuristic approaches in general.
© 1986 by Springer-Verlag
Proceedings of the Second International Logic Programming Conference, pages 263-276. University of Uppsala, Sweden, 1984. (With Jean-Louis Lassez and Michael Maher.)
The treatment of soundness, weak completeness and strong completeness of various logic program resolution strategies with respect to success and failure is generalized and considerably simplified. This is made possible by using the full power of the unification theorem which allows a reduction to a simple canonical case. The results can then be established in a natural and straightforward manner. We also indicate how the unification theorem can be used to simplify the proof of the completeness of the negation as failure rule. Finally we note that the treatment introduced in this paper applies to other clausal forms.
© 1984 by University of Uppsala.