Logic & Formal Reasoning
Modal and Temporal Logics-Based Planning for Open Networked Multimedia Systems
The titles of the five symposia were Modal and Temporal Logics-Based Planning for Open Networked Multimedia Systems Narrative Intelligence Psychological Models of Communication in Collaborative Systems Question-Answering Systems Using Layout for the Generation, Understanding, or Retrieval of Documents This article concludes with a previously unpublished report on the 1998 AAAI Fall Symposium on AI and Link Analysis. This symposium provided a forum for researchers involved in using formal methods and in design of networked multimedia systems and adaptivereactive systems to identify common ground, relevant experiences, applications, open problems, and possible future developments. To support intelligent and interactive multimedia applications, there's a need to tailor systems to possess and use knowledge about the application domain, user-requirement tasks, the context of interaction, communication, and performance parameters. Temporal and modal logics have been used to reason about time, action, and adaptive change and to program and verify networked systems. The 1999 American Association for Artificial Intelligence Fall Symposium Series was held Friday through Sunday, 5-7 November 1999, at the Sea Crest Oceanfront Resort and Conference Center.
Veronica Dahl
The 1993 International Logic Programming Symposium was held in Vancouver, British Columbia, on 26-29 October. It presented the state of the art in logic programming, emphasizing the deliberate interaction with other fields, in particular, humanistic fields. Topics covered at the symposium included algorithmic analysis, programming methodologies, semantic analysis, deductive databases, and programming language design. The years of unrelenting development by these pioneers and other wonderful people have brought the field to a stage of maturity that makes more deliberate interactions with other fields possible and desirable and that gives us enough perspective to consider our field from wider viewpoints, such as the philosophical. The 1993 International Logic Programming Symposium, held in Vancouver, British Columbia, on 26-29 October, presented the state of the art in logic programming and also emphasized these other viewpoints.
Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing
The SAT Conference on Theory and Applications of Satisfiability Testing was held in Lisbon, Portugal, 28-31 May 2007. The conference, which attracted a record-breaking 80 participants, featured 34 papers and two invited presentations. The venue also included the SAT competition, the QBF evaluation, the PB evaluation, and the MAX-SAT evaluation. Moreover, SAT and extensions of SAT find many practical applications, including planning, software and hardware model checking, bioinformatics, equivalence check ing, test-pattern generation, software package installation, and cryptography. The annual SAT conference is now widely recognized as "the venue" for AI Magazine Volume 28 Number 4 (2007) ( AAAI) This year marked the tenth SAT meeting.
The International SAT Solver Competitions
The International SAT Solver Competition is today an established series of competitive events aiming at objectively evaluating the progress in state-of-the-art procedures for solving Boolean satisfiability (SAT) instances. Over the years, the competitions have significantly contributed to the fast progress in SAT solver technology that has made SAT a practical success story of computer science. This short article provides an overview of the SAT solver competitions. In addition to its theoretical importance, major advances in the development of robust implementations of decision procedures for SAT, SAT solvers, have established SAT as an important declarative approach for attacking various complex search and optimization problems. Modern SAT solvers are routinely used as core solving engines in vast numbers of different AI and industrial applications.
The Answer Set Programming Competition
The competition consists of two main tracks: the ASP system track and the model and solve track. The traditional system track compares dedicated answer set solvers on ASP benchmarks, while the model and solve track invites any researcher and developer of declarative knowledge representation systems to participate in an open challenge for solving sophisticated AI problems with their tools of choice. This article provides an overview of the ASP Competition series, reviews its origins and history, giving insights on organizing and running such an elaborate event, and briefly discusses the lessons learned so far. The main goal of ASP is to provide a versatile declarative modeling framework with many attractive characteristics. These features allow turning -- with little to no effort -- problem statements of computationally hard problems into executable formal specifications, also called answer set programs.
The CADE ATP System Competition -- CASC
The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic automated theorem-proving (ATP) systems for classical logic -- the world championship for such systems. CASC provides a public evaluation of the relative capabilities of ATP systems, and aims to stimulate ATP research toward the development of more powerful ATP systems. Over the years CASC has been a catalyst for impressive improvements in ATP. CASC is held at the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR, which replaces CADE on alternate years) each year. These conferences are the major forums for the presentation of new research in all aspects of automated deduction. The evaluation is in terms of the number of problems solved, the number of solutions output, and the average run time for problems solved in the context of a bounded number of eligible problems, chosen from the TPTP Problem Library (Sutcliffe 2009), and a CPU time limit for each solution attempt. One purpose of CASC is to provide a public evaluation of the relative capabilities of ATP systems.
Workshop on Defeasible Reasoning with Specificity and Multiple Inheritance
A workshop on defeasible reasoning with specificity was held under the arch in St. Louis during April 1989, with support from AAAI and McDonnell Douglas, and the assistance of Rockwell Science Center Palo Alto and the Department of Computer Science of Washington University. The workshop brought together proposers of systems of nonmonotonic or defeasible reasoning that exhibited subclass or specificity defeat. There were twenty invited participants. The program committee (David Etherington, Hector Geffner, and David Poole) also invited an equal number of participants from those responding to the call for participation. One third of the attendees of the workshop came from abroad.
Woody Bledsoe
Woodrow Wilson (Woody) Bledsoe died on 4 October 1995 of ALS, more commonly known as Lou Gehrig's disease. Woody was one of the founders of AI, making early contributions in pattern recognition and automated reasoning. He continued to make significant contributions to AI throughout his long career. His legacy consists not only of his scientific work but also of several generations of scientists who learned from Woody the joy of scientific research and the way to go about it. Woody's enthusiasm, his perpetual sense of optimism, his can-do attitude, and his deep sense of duty to humanity offered those who knew him the hope and comfort that truly good and great men do exist. Woody was one of the founders of AI, making early contributions in pattern recognition and automated reasoning. He continued to make significant contributions to AI throughout his long career. His legacy consists not only of his scientific work but also of several generations of scientists who learned from Woody the ...
1614
Where Are the Semantics in the Semantic Web? The most widely accepted defining feature of the semantic web is machine-usable content. By this definition, the semantic web is already manifest in shopping agents that automatically access and use web content to find the lowest air fares or book prices. However, where are the semantics? Most people regard the semantic web as a vision, not a reality--so shopping agents should not "count."
Introduction to the COMTEX Microfiche Editor of Memos from the Stanford Artificial Intelligence Laboratory
Stanford, California 94305 THE STANFORD Artificial Intelligence Project, later known as the Stanford AI Lab or SAIL, was created by Prof. John McCarthy shortly after his arrival at Stanford in 1962. As a faculty member in the Computer Science Division of the Mathematics Department, McCarthy began supervising research in artificial intelligence an,d timesharing systems with a few students. From this small start, McCarthy built a large and active research organization involving many other faculty and research projects as well as his own. There is no single theme to the SAIL memos. They cannot be easily categorized because they show a diversity of interests, resulting from the diversity of investigators and projects. Nevertheless, there are some important dimensions to the research that took place in the Al Lab that I will try to put in historical context in this brief introduction. 'I thank John McCarthy, especially, for answering numerous questions and for reading the whole introduction for accuracy His advice, "don't try to unify the reports," preempted any contrary obligations I felt to readers Les Earnest was very helpful in giving me names and dates, providing photographs, and reading this account. I also appreciate time and information from Ed Feigenbaum, Raj Reddy, Jerry Feldman, Cordell Green, Roger Schank, Tony Hearn, Bill McKeeman and Nils Nilsson 2Readers should note that since the early 1970's there have been two centers of AI research at Stanford, SAIL and the Heuristic Programming Project (HPP). The HPP memos are not discussed here and are not part of the COMTEX collection. Instead, I have recounted some of the early history of SAIL, and its prehistory, as I remember it and have learned it from others' memories.' It is undesirable (and impossible besides) to try to unify the reports into a single theme, or to unify the research themes into a single purpose. Therefore, this mini-history mentions several themes (and a few names) from the 1960's and 70's that set the major directions of AI research at Stanford. Many of these early interests, such as robotics, have been vigorously pursued ever since. Omissions are unintentional, and should not be interpreted as having implied significance. The present collection is a complete set of SAIL memos from the beginning of the lab until 1982.2 The technical memos in the SAIL series are not of uniform quality. Some of these papers are preprints of journal articles of lasting interest. Others constitute documentation on how to use the system. Still others are hastily written drafts describing work in progress at the time.