DAI-List Digest Wednesday, 7 April 1993 Issue Number 114 Topics: Thesis on Distributed Automated Deduction DAI Papers at FLAIRS-93 Request for info on DAI tools and testbeds Request for information on distributed reason maintenance IJCAI'93 Workshop on Knowledge Sharing and Information Interchange Administrivia: Please send submissions to DAI-List@mcc.com. Send other requests, such as changes in your e-mail address, to DAI-List-Request@mcc.com. ---------------------------------------------------------------------- Date: Sat, 27 Mar 93 18:12:26 +0100 From: Bonacina Maria Paola Subject: Thesis on Distributed Automated Deduction Dear readers, I am working in distributed automated deduction. By automated deduction I mean theorem proving in first order logic with equality, with inference rules like resolution, paramodulation, i.e., "expansion" rules, and subsumption and simplification, i.e., "contraction" (or deletion) rules. (This is not meant to be exclusive.) By distributed automated deduction, I mean the possibility of having several concurrent, asynchronous, deductive processes working to the solution of the given theorem proving problem. I recently graduated from SUNY at Stony Brook with a thesis on this subject. For those interested, I am appending an extended version of my thesis abstract. TITLE: Distributed Automated Deduction AUTHOR: Maria Paola Bonacina ADVISOR: Prof. Jieh Hsiang SCHOOL: Dept. of Computer Science, SUNY at Stony Brook GRADUATION DATE: December 1992 ABSTRACT: This thesis comprises five main contributions: 1. an abstract framework for theorem proving, 2. an analysis of the parallelizability of theorem proving strategies, 3. a methodology for parallel theorem proving in a distributed environment, termed deduction by "Clause-Diffusion", 4. a study of special topics in distributed deduction with contraction 5. and an implementation, the theorem prover "Aquarius", of the Clause-Diffusion methodology. 1. In our abstract framework, Knuth-Bendix type completion procedures are treated as semidecision procedures for theorem proving, rather than procedures to generate confluent systems. A theorem proving derivation is conceived as a process of reducing a proof of the target or goal. Accordingly, all the fundamental notions of contraction inference rules, redundancy of clauses, refutational completeness of the inference mechanism and fairness of the search plan, are defined in a target-oriented fashion. The most important feature of our framework is that it provides the first notion of fairness for theorem proving, which is weaker than the fairness property required to generate confluent systems. A weaker fairness requirement means that fewer inference steps are necessary. Therefore, a weaker fairness requirement is a theoretical precondition to the design of more efficient theorem proving strategies. 2. We classify three classes of theorem proving strategies, i.e., Subgoal-reduction strategies, Expansion-oriented strategies, and Contraction-based strategies, and three types of parallelism, i.e. parallelism at the Term level (fine grain), parallelism at the Clause level (medium grain) and parallelism at the Search level (coarse grain). We analyze the applicability of these three types of parallelism to strategies in the three above classes with respect to several issues, including: how dynamic is the data base of clauses during the derivation, the possibility of conflicts between parallel inferences, the duplication of clauses, whether the memory is shared or distributed, and more. The result of this analysis is that while subgoal-reduction strategies are amenable to all three types of parallelism, and expansion-oriented strategies still admit both parallelism at the clause level and parallelism at the search level, only parallelism at the search level is suitable for contraction-based strategies. The abundant use of contraction rules, which makes these strategies so efficient in sequential execution, makes their parallelization more challenging. 3. The Clause-Diffusion methodology realizes parallelism at the search level, by having concurrent, asynchronous, deductive processes searching in parallel the search space of the problem. The search space is partitioned among the processes by distributing the clauses and by subdividing certain classes of inferences. The processes communicate by exchanging data and they halt successfully as soon as one of them finds a proof. Policies for distributing the clauses and for scheduling inference and communication steps complete the picture. While the Clause-Diffusion methodology applies to theorem proving in general, it has been designed to provide solutions to the problems in the parallelization of contraction-based strategies, since they have been among the most successful. We describe backward contraction, i.e., the task of maintaining clauses reduced in a dynamically changing data base, as the main obstacle in parallel theorem proving with contraction. If a finer granularity of parallelism is adopted, e.g., parallelism at the clause level in shared memory, this difficulty appears as a write-bottleneck, which we have called the Backward Contraction Bottleneck. The Clause-Diffusion approach avoids this problem by adopting a mostly distributed memory and new distributed global contraction schemes. 4. We have given a definition of distributed derivations and characterized their fairness requirements, including fairness of inferences and fairness of communication. We have shown that the Clause-Diffusion methods are fair. Also, we have observed that the uncontrolled application of subsumption in a distributed data base may violate the fairness and the monotonicity - a dual property of soundness - of distributed derivations. This discovery has propelled a reexamination of the subsumption inference rule, which we view as a replacement rule, rather than a deletion rule. Our new distributed subsumption inference rule preserves both fairness and monotonicity, without reducing the contraction power of subsumption. 5. We conclude with the description of the distributed theorem prover Aquarius, including some experiments, and with directions for future research, such as the design of Parallel Search Plans. ------------------------------ Date: Wed, 24 Mar 1993 09:12-0600 From: Michael N. Huhns Subject: DAI Papers at FLAIRS-93 1993 Florida AI Research Symposium on Knowledge-Based Systems April 18-21, 1993 Ft. Lauderdale, FL "The Advantages of Conflict in Multiagent Systems," Todd Lehman, Florida Institute of Technology "Cooperative Intelligent Information Systems Integrating Knoledge-Based Systems," H. Grashoff and J. Long, City University, United Kingdom "A Language-Based Computational Model of Social Competence," R. Morris, Florida Institute of Technology "Parallel CLIPS for Concurrent Hypercube Architectures," L. Hall, L. Prasad, and E. Jackson, University of South Florida "Metacomputing for Large Databases and Knowledge Bases," Patrick Bobbie, University of West Florida For registration info, contact edmunds@acc.fau.edu ------------------------------ From: Gerhard Kraetzschmar Subject: Request for info on DAI tools and testbeds Date: Thu, 1 Apr 93 16:56:05 +0100 Hello netters and news readers! I am in the process of doing a survey in Distributed AI regarding two specific areas of DAI software/systems: - tools - testbeds As AI people's understanding of tools and testbeds can be quite different (experience :-)), I give a characterization of the kind of things that in my opinion qualify for these two areas below (after the signature). I am very grateful for every hint I get. For both kinds of systems, please specify in every case - the name of the system - a contact (author, implementer, provider of further info) - an abstract of its functionality and, if possible - implementation language and state (in use, in development)) - availability (commercial/proprietary/public domain) - how to use it - how to integrate it in DAI sw systems - other relevant info (ftp source: host, Internet-Id, dir) Please respond via email to gkk@forwiss.uni-erlangen.de. I will collect the responses and mail/post a summary to all the newsgroups/lists I posted this article to (probably around end of April). Also, most likely a report from our research institute will be available on the topic. Thanks in advance for your cooperation! So long, Gerhard K. Kraetzschmar FORWISS Email: kraetzschmar@forwiss.uni-erlangen.de Am Weichselgarten 7 Telephone: intl.+49-9131-691-193 8520 Erlangen-Tennenlohe Telefax: intl.+49-9131-691-185 Federal Republic of Germany Things that qualify for DAI tools: The general idea here is to substantially reduce the effort needed for implementing DAI systems, e.g., by providing a framework for multiple agents communicating via a specific protocol, etc. That is, I look for software systems and utilities that implement specific DAI concepts, technologies or architectures, such as (just a few examples) - an implementation of the contract net protocol - an implementation of a distributed TMS - an system that allows for easy configuration and programming of multi-agent systems with a specific architecture - the implementation of a mechanism for enabling/ensuring cooperative behavior between agents - the implementation of a mechanism for resolving conflicts between competing/non-competing agents Note, that the software should provide significantly more support than e.g., CommonLisp + C interface + TCP-IP + (lightweight) processes, and one or more DAI technologies should be more or less directly applicable. Things that qualify for DAI testbeds: Software environments, that allow testing and evaluation of DAI systems, such as multiagent systems (MAS) and (cooperative,) distributed problem solvers ((C)DPS). They must provide functionality to define and simulate an environment for the DAI system to be evaluated in, as well as an interface to the DAI system. Certain restrictions, like "can interface only via TCP/IP" or "good only for LISP-implemented agents" are acceptable. The testbed must provide functionality to perform experiments with a DAI system under varying environment conditions, record internal data of the DAI system during experiments for later evaluation, and enable the experimenter to repeat experiments and reconstruct critical or interesting situations. An essential criterion is that the testbed should allow (and actually has been used) to test and evaluate more than one specific DAI system or architecture. Probably there are more testbeds around that do NOT meet this essential criterion; if this is the case, please send info, but do clearly state that testbed X has been developed to evaluate DAI system Y, but (in theory/with some work/easy but not done) could be used to evaluate DAI system Z as well. ------------------------------ From: Gerhard Kraetzschmar Subject: Request for information on distributed reason maintenance Date: Thu, 1 Apr 93 17:01:12 +0100 Hello netters and news readers! Together with several colleagues I am working on -> distributed reason maintenance (reason maintenance in distributed systems, e.g., multiagent systems) and -> distributed belief revision (belief revision in distributed systems, e.g., multiagent systems). We know of several other efforts in this regard, including - DTMS (Bridgeland/Huhns) - BRTMS (Horstmann) - DATMS (Mason/Johnson) and, e.g., the thesis of Afzal Ballim announced previously here. However, we appreciate any further helpful comments or references. Any hint is welcome! Please respond via email (do not post to this list or newsgroup) to gkk@forwiss.uni-erlangen.de I will collect the responses and mail/post a summary to all the newsgroups/lists I posted this article to. Thanks in advance for your cooperation! So long, Gerhard K. Kraetzschmar FORWISS Email: kraetzschmar@forwiss.uni-erlangen.de Am Weichselgarten 7 Telephone: intl.+49-9131-691-193 8520 Erlangen-Tennenlohe Telefax: intl.+49-9131-691-185 Federal Republic of Germany ------------------------------ From: Philippe Gobinet Subject: IJCAI Workshop on Knowledge Sharing and Information Interchange Date: Thu, 1 Apr 1993 07:07:23 -0800 CALL FOR PARTICIPATION IJCAI'93 Workshop on Knowledge Sharing and Information Interchange August 28th, 1993 - Chambery, FR Connecting Knowledge Based Systems (KBSs) with conventional software or with other KBSs poses problems of knowledge sharing and information interchange. Possible solutions of knowledge representation problems are the subject of intense discussions in the American AI Community and in Europe through European Community ESPRIT funded research projects, academic research, and the newly formed EuroKnowledge initiative. This one-day Workshop during IJCAI'93 will confront the different approaches on Knowledge Sharing and Information Interchange and promote communication between researchers. The following subtopics are of interest for the Workshop (others can be considered): * a common language for knowledge interchange (scope, semantics, syntax), * translation/mapping from a formalism to the common language, * generic ontologies, * use of a single knowledge representation formalism for the development of all KBSs, * reuse of existing KBs (methodological issues, standards). * potential of a standard query language/communication protocol. Organization: The maximum number of attendees is 35. The language is English. For each subtopic, several position statements will be made. Follow up discussions are then planned. The aim of this workshop is to promote an open exchange of ideas rather than a formal speaker/audience format. A round table will be organized to conclude the day. The Contact Person will assure the organization of minutes taking and production of the synthesis of the Workshop. Several overviews will be added to this report: * the DARPA Knowledge Sharing Effort, * the EuroKnowledge initiative, * the IMKA effort. Submission: People wishing to present a communication (about 15 minutes) at the workshop should submit a short position paper (about 1700 words). Other persons wishing to attend the workshop should submit a short presentation paper (about 500 words) describing why their contribution to the workshop would be of interest (i.e. the research they have been conducting in the domain or in a related domain). Three copies (hard copy, Latex on e-mail or fax) have to be sent to the contact person. Papers must include: author's name(s), affiliation, main field of specialization, complete postal address, phone and fax number, and e-mail. Schedule: position paper, intention of participation: April 23 Notifications: May 3 Final copies of position papers: July 2 Practical information: According to the IJCAI'93 organization, each workshop attendee must have registered for the main conference. The fee of the workshop are an additional 300 FF (about 55 $) Organization Committee: Giuseppe Attardi, University of Pisa, Italy Tim Finin, University of Maryland, USA Mike Genesereth, Stanford University, USA Douglas B. Lenat, MCC, USA Ramon Lopez de Mantaras, Blanes Center of Advanced Studies, Spain Don McKay, Paramax Systems Corporation, USA Bob Neches, USC/ISI, USA Catherine Peyralbe, Cap Gemini Innovation (chair), France Contact Person for further information: Catherine Peyralbe CAP GEMINI INNOVATION 86-90 rue Thiers, 92513 Boulogne Billancourt Cedex FRANCE Tel: +33 49 10 52 71 Fax: +33 49 10 06 15 E-mail: peyralbe@capsogeti.fr ------------------------------ End of DAI-List Digest Issue #114 *********************************