One of the most widely-used and successful approaches to increasing the efficiency of general-purpose automated reasoning systems has been that of integrating special-purpose reasoning systems into them, resulting in what are often called hybrid reasoning systems. Though the resulting hybrid reasoning systems are appealing, their construction and analysis can be difficult [17]. Our research helps to remedy this problem for a particular class of hybrid reasoners that we have identified and dubbed "substitutional reasoners". Substitutional reasoners share certain architectural features; most notably they (1) operate on a language that contains a distinguished set of symbols for representing constraints on the values over which quantified variables range, and (2) employ a special purpose reasoning system to test the satisfiability of these constraints. One of the distinguishing features of substitutional reasoners is that the constraints are manipulated exclusively by the special-purpose reasoner.
Though the substitutional architecture has been one of the most common and successful architectures for hybrid reasoning, our research is the first to identify these reasoners as a single class and to investigate their common properties and the general principles that underly them. Our results support a framework that enables the systematic production of substitutional reasoners and their completeness proofs from certain kinds of non-hybrid reasoners and their completeness proofs [15, 20]. Within the substitutional framework we have studied reasoning systems for knowledge retrieval, constraint logic programming, modal logic deduction [21], parsing feature-based grammars [16], inductive learning with background information [25], and planning in temporally rich domains.
In contrast to our results on deduction with constraints, which have been obtained by abstracting away from algorithmic issues and concentrating on architectural issues, we are taking a growing interest in constraint-solving algorithms. Our previous work has studied sorted unification, an operation that lies at the heart of all automated deduction systems for sorted logic, and which can be seen as jointly solving membership and equational constraints [18]. Our current work studies the relationship of deduction to the problem of simultaneously satisfying a set of symbolic constraints on finite domains [19]. Future efforts will concentrate on integrating deductive methods and traditional constraint satisfaction techniques to effectively solve large constraint satisfaction problems.
The aim of this project is to develop, analyse and evaluate methods for generating implied constraints automatically.
We expect such methods to become a vital component of the next generation of constraint satisfaction toolkits. One of the key ideas will be to combine theorem proving techniques with constraint satisfaction algorithms. Constraint satisfaction is a highly successful technology for tackling a wide variety of search problems including resource allocation, transportation and scheduling. Several recent studies show that implied constraints added by hand to a problem representation can lead to significant reductions in search. There has, however been little research on how to generate such implied constraints automatically outside of a highly focused domain like planning.
Research in multi-agent systems tends to focus on cooperative problem solving domains, where autonomous agents start with a common goal and then acquire social attitudes before forming a group. We have developed a more comprehensive coordination framework in which social activity is modelled from an individualistic point of view; [3]. In this model agents reason about their dependence relations in the cooperative domain. Using a protocol that we have defined; [1, 2], the agents exchange offers according to certain "social" strategies until they reach a deal. The resulting conditional commitments oblige them to abide by agreements in societies (or teams if the rooted goals are one and the same). Joint plans are seen as deals and team activity is seen as a special case of social activity.
Our recent work; [4, 5, 6] draws upon and extends this research
in several ways: The agent negotiation mechanism has been substantially improved with the analysis of goal structures.
Coordination is seen as the automatic search of "fair" agreements through the "solution-trees" of both agents. The
model is now applicable both to cooperative and non-cooperative domains. The emphasis is put on common interests, not
on common goals. Notions traditionally involved in cooperative problem solving, such as help and joint responsibility,
are applied to any interaction situation without appealing to inherently social notions.
Our future work will attempt to reduce the complexity of the model, both in the language and in the coordination
mechanism. In addition the model will be extended to multi-agent systems with more than two agents. This will require
an analysis of roles (such as mediator, arbiter, witness and representative) and new phenomena (such as alliances,
coalitions and organisations).
Z, a formal specification language based upon Zermelo-Frankal set theory, is used extensively in both academia and industry. Several tools have been developed for reasoning about Z specifications, but they all lack substantial facilities for inductive reasoning. We are developing such a reasoning assistant for Z [13]. Initial work has been concerned with free-type induction, and its interaction with Z's types and partial functions [11]. Subsequent work will be concerned with utilising the concept of "ordered covering" as the basis for more general inductive reasoning, and with combining aspects of both the classical and rewrite-based approaches to proof by induction [12]. In particular, our approach will include the classical induction "on variables" and use of heuristics, and the rewrite-based induction "on subterms" and simultaneous proofs of multiple conjectures. In this way we not only are developing an inductive reasoner for Z but are furthering our understanding of the automation of proof by induction.
To ensure that our reasoning principles and strategies are appropriate for Z, we are implementing them in CADiZ, an interactive reasoning tool for Z developed at the University of York [26]. We will demonstrate the utility of the resulting system by using it to construct a broad range of proofs, including some of practical importance to computer security, safety-critical systems and compiler correctness.
The goal of an Inductive Logic Programming (ILP) system is to form a hypothesis, expressed as a logic program, that accounts for a given set of examples. Though ILP systems have been applied with great success to a number of real-world problems, they inherit some of the shortcomings inherent in the traditional logic programming paradigm. In particular, with traditional logic programming languages it is difficult to naturally express computations over domains other than the Herbrand universe (the set of variable-free logical terms). Thus logic programming languages usually require extra-logical constructions to express operations such as arithmetic ones. Consequently, the major results of ILP, which are formulated for pure logic programs, cannot be applied directly to non-Herbrand domains. Constraint logic programming generalises the ideas of ordinary logic programming to allow computation over non-Herbrand domains in a principled and natural manner. This is achieved by replacing the unification procedure of ordinary logic programming with more general constraint-solving mechanisms.
Our research is attempting to take the major ideas and results from ILP and generalise them to the learning of constraint logic programs [7]. Our goal is to demonstrate that the resulting enterprise-Inductive Constraint Logic Programming-provides useful methods for learning in non-Herbrand domains such as numerical domains. One significant problem that we have addressed [9] is how to choose the numerical constants that appear in induced constraints, such as the constant "3" in the constraint "X £ 3".
The hypotheses induced by Inductive Logic Programming (ILP) systems are logic programs that comprise a finite set of a logical clauses. Much recent work in ILP examines the question of how to find an individual clause of high quality-that is, one which does a good job of accounting for the given examples. Significantly less attention has been paid to the question of how to select a set of such clauses to form a high quality hypothesis. The usual method is to select clauses in a greedy manner: start with the empty set of clauses and repeatedly add the clause that most improves the quality of the set. Our research has developed a non-greedy method for selecting the clauses that form a hypothesis [8]. The key feature of our "cautious" method is that it draws a clear distinction between the task of finding clauses and the task of combining them to form a hypothesis. Through empirical analysis we are currently attempting to gain further insight into the relationship between our cautious method and existing greedy methods.
Ambiguity arises at all levels of linguistic knowledge-morphology, phonology, syntax, semantics and discourse. A natural language processing system incurs heavy penalties if its implementation does not employ a representation that is largely non-committal. Unfortunately, current state-of-the-art grammatical systems are overly committal in expressing certain linguistic phenomena, such as word order. To address these shortcomings we have formulated and implemented special-purpose constraint logics [14] that incorporate, in particular, set-valued feature descriptions [22, 23] and complex word-order constraints [24]. In addition, to provide a basis for investigating resource-sensitive linguistic theories we have developed hybrid constraint-based extensions to the Lambek calculus [10].
We are now investigating deductive systems for efficiently handling probabilistically ranked semantic ambiguities. Such a system could be used to obtain the most probable interpretation of a highly ambiguous representation. Our future work will concentrate on formulating a general purpose constraint-solving scheme suitable for specifying complex constraint-based grammars for use in a generic parsing and generation architecture. We will also attempt to develop a hybrid constraint logic that combines constraint reasoning with probabilistic information. The goal would be to specify and implement a formalism that subsumes existing constraint-based formalisms.
One of the major bottlenecks in developing practical natural-language processing systems is the time required to construct large scale lexicons/grammars containing the complex information necessary for machine understanding of language. Though many researchers have shifted their attention to the problem of (semi-)automatically acquiring lexicons/grammars, their efforts have focused on simple grammatical formalisms capable of only shallow linguistic processing. Our research aims to develop methods for the (semi-)automatic acquisition of lexicons/grammars for modern, powerful constraint-based grammatical formalisms.
Modern constraint-based grammatical theories, such as Head-driven Phrase Structure Grammar (HPSG), employ a complex range of constraints for representing linguistic knowledge. On the one hand, such a rich grammatical theory makes it possible to write grammars that contain very rich linguistic knowledge. On the other hand, it also makes it difficult to automatically acquire such grammars from large corpora. Thus capturing the linguistic reasoning mechanisms in a simpler grammatical system is essential for the (semi-)automatic acquisition of grammars. To this end, em am currently interested in categorial grammar approximations of HPSG such as extending hybrid constraint-based categorial grammars [10] with word-ordering constraints [24].
Recent work in inductive machine learning have successfully been applied to the learning of morphological rules and learning of simple context-free grammar systems. We have successfully applied our decision-list learning system for the automatic induction of Slovene morphological rules. In addition to this, we are currently exploring the application of such techniques for the learning of grammars which are based on complex grammatical theories such as categorial grammars and HPSG.
Typed feature formalisms are (constraint) logic programming languages that are designed for implementing constraint-based grammatical theories such as Head-driven Phrase Structure Grammar (HPSG). Currently, most such implementations are written in Prolog. Though perfectly adequate for small-scale grammars, such implementations are inadequate for developing large-scale industrial strength grammars. To address this issue we are currently developing techniques for compiling typed feature-structure based grammars into compact instructions that can be efficiently executed by an abstract machine. Our techniques are based on partial evaluation and bit-vector based representations.
[1] Alonso, E.
A Formal Framework for the Representation of Negotiation Protocols.
Inteligencia Artificial, 3 pp.30-49,
1997.
[2] Alonso, E.
A Logical Representation of a Negotiation Protocol for Autonomous Agents.
In Proc. DAIMAS-97, pp. 32-43, St. Petersburg,
1997.
[3] Alonso, E.
An Uncompromising Individualistic Formal Model of Social Activity.
In Proc. FoMAS-97, Coventry,
The UK Special Interest Group on Foundations of Multi Agent Systems.
1997.
[4] Alonso, E.
Groups and Societies: One and the Same Thing?
In Proc. IBERAMIA-98, Lisbon,
1998. Submitted.
[5] Alonso, E.
How Agents Negotiate Societies.
In Proc. ICMAS-98, Paris,
1998. Submitted.
[6] Alonso, E.
Searching for Coordination in Social MAS.
In Proc. ECAI-98, Brighton,
1998. Submitted.
[7] Anthony, S. and Frisch, A. M.
Towards Inductive Constraint Logic Programming.
In Gent, em., editor,
Working Notes, 1996 AISB Workshop on Automated Reasoning:
Bridging the Gap between Theory and Practice,
pp. 3-4, Brighton, Society for the Study of Artificial Intelligence and Simulation of Behavior,
1996.
[8] Anthony, S. and Frisch, A. M.
Cautious Induction in Inductive Logic Programming.
In Lavra, N. and Deroski, S., editors,
Inductive Logic Programming: 7th International Workshop, ILP-97,
pp. 45-60, Prague, Czech Republic, Springer Verlag,
1997.
[9] Anthony, S. and Frisch, A. M.
Generating Numerical Literals During Refinement.
In Lavra, N. and Deroski, S., editors,
Inductive Logic Programming: 7th International Workshop, ILP-97,
pp. 61-76, Prague, Czech Republic, Springer Verlag,
1997.
[10] Dörre, J. and Manandhar, S.
On Constraint-based Lambek Calculi.
In Blackburn, P. and de Rijke, M., editors,
Specifying Syntactic Structures.
CSLI Publications, Stanford, CA,
to appear.
[11] Duffy, D. A., Frisch, A. M. and Toyn, em.
Free-Type induction in CADiZ.
Available from the Department of Computer Science, University of York
at http://www.cs.york.ac.uk/isg/papers/,
1997.
[12] Duffy, D.
Proof by Induction in Equational Theories.
PhD thesis, Department of Computer Science, University of Strathclyde,
1992.
[13] Duffy, D. A., Frisch, A. M. and Toyn, em.
Proof by Induction: Bridging the Gap between Proof Theory and Practical Automated Proof Systems.
In Fisher, M., editor,
Working Notes, 1997 AISB Workshop on Automated Reasoning:
Bridging the Gap between Theory and Practice,
Manchester, Society for the Study of Artificial Intelligence and Simulation of Behavior,
1997.
[14] Erbach, G., van der Kraan, M., Manandhar, S., Ruessink, H., Skut, W. and Thiersch, C.
Extending Unification Formalisms.
In Second Language Engineering Convention,
pp. 161-168, London, England,
1995.
[15] Frisch, A. M.
The Substitutional Framework for Sorted Deduction: Fundamental Results on Hybrid Reasoning.
Artificial Intelligence, 49 pp. 161-198,
1991.
[16] Frisch, A. M.
Feature-Based Grammars as Constraint Grammars.
In Cole, J., Green, G. M. and Morgan, J. L., editors,
Linguistics and Computation, pp. 85-100. CSLI Publications, Stanford, CA,
1995.
[17] Frisch, A. M. and Cohn, A. G.
Thoughts and Afterthoughts on the 1988 Workshop on Principles of Hybrid Reasoning.
AI Magazine, 11(5) pp. 77-83,
1991.
[18] Frisch, A. M. and Cohn, A. G.
An Abstract View of Sorted Unification.
In Kapur, D., editor,
Proceedings of the Eleventh International Conference on Automated Deduction,
pp. 178-192, Saratoga Srpings, NY,
1992.
[19] Frisch, A. M. and Dumbill, E. J.
A Solving Constraint Satisfaction Problems with MV-Resolution: Initial Investigations.
In Ireland, A., editor,
Working Notes, 1995 AISB Workshop on Automated Reasoning:
Bridging the Gap between Theory and Practice,
pp. 35-36, Sheffield, Society for the Study of Artificial Intelligence and Simulation of Behavior.
1995.
[20] Frisch, A. M. and Page Jr., C. D.
Building Theories into Instantiation.
In Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence,
pp. 1210-1216, Montreal, Canada,
1995.
[21] Frisch, A. M. and Scherl, R. B.
A General Framework for Modal Deduction.
In Allen, J., Fikes, R. and Sandewall, E., editors,
Principles of Knowledge Representation and Reasoning:
Proceedings of the Second International Conference,
pp. 196-207. Morgan Kaufman, San Mateo, CA,
1991.
[22] Manandhar, S.
Relational Extensions to Feature Logic: Applications to Constraint Based Grammars.
PhD thesis, Department of Artificial Intelligence, University of Edinburgh,
1993.
[23] Manandhar, S.
An Attributive Logic of Set Descriptions and Set Operations.
In 32nd Annual Meeting of the Association for Computational Linguistics,
pp. 255-262, Las Cruces, New Mexico,
1994.
[24] Manandhar, S.
Deterministic Consistency Checking of LP Constraints.
In Seventh Conference of the European Chapter of the Association for Computational Linguistics
(EACL'95),
pp. 165-172, Dublin, Ireland,
1995.
[25] Page Jr., C. D. and Frisch, A. M.
Generalization and Learnability: A Study of Constrained Atoms.
In Muggleton, S. H., editor,
Inductive Logic Programming,
chapter 2, pp. 29-61. Academic Press, London,
1992.
[26] Toyn, em. and McDermid, J.
CADiZ: An Architecture for Z Tools and its Implementation.
In Comer, D. and Wellings, A., editors,
Software: Practice & Experience,
pp. 305-330,
1995.