Computational Logic has outgrown its humble beginnings and early expectations by far: with close to ten thousand people working in research and development of logic-related methods, with several dozen international conferences and workshops addressing the growing richness and diversity of the field, and with the foundational role and importance these methods now assume in mathematics, computer science, artificial intelligence, cognitive science, linguistics and many engineering fields — where logic-related techniques are used inter alia to state and settle correctness issues — the field has diversified in ways that the pure logicians working in the early decades of the last century could have hardly anticipated. Dating back to its roots in Greek philosophy as presented in the works of Aristotle, logic has grown in richness and diversity over the centuries to finally reach the modern methodological approach expressed in the work of Frege. Logical calculi, which capture an important aspect of human thought, are now amenable to investigation with mathematical rigour; and the beginning of this century saw the influence of these developments in the foundations of mathematics, in the work of Hilbert, Russell and Whitehead, in the foundations of syntax and semantics of language, and in philosophical foundations expressed most vividly by the logicians in the Vienna Circle. Picking up on these developments and on the early dreams of mechanised reasoning, the Dartmouth Conference in 1956 raised explicitly the hopes for the new possibilities that the advent of electronic computing machinery offered: logical statements could now be executed on a machine with all the far-reaching consequences that ultimately led to logic programming, deduction systems for mathematics and engineering, logical design and verification of computer software and hardware, deductive databases and software synthesis as well as logical techniques for analysis in the field of mechanical engineering. In this way the growing richness of foundational and purely logical investigations that had led to such developments as:
- first order calculi
- type theory
- and higher order logic
- non-classical logics
and others, was extended by new questions and problems in particular in computer science and artificial intelligence, leading to:
- denotational semantics for programming languages
- nonmonotonic reasoning
- logical foundations for computing machinery such as CSP, p-Calculus and others for program verification
- logical foundations for cognitive robotics
- syntax and semantics for natural language processing
- logical foundations of databases
- linear logics
- probabilistic reasoning and uncertainty management
- logical foundations and its relationship to the philosophy of mind,
and many others.
This growing diversity is reflected in the numerous conferences and workshops that address particular aspects of the fields mentioned.
For example, only twenty years ago, there was just one international conference on automated deduction (later to be called CADE). Today there is not only CADE but among others: LICS (Logic in Computer Science), RTA (Rewriting Techniques and Applications),LPAR (Logic Programming and Automated Reasoning), the TABLEAUX Conference, TPHOL (Theorem Proving in Higher Order Logic), UNIF (Unification Workshop), and FTP (First Order Theorem Proving), each of which is held regularly with its own set of proceedings and supported by a mature community. Frequently these conferences are backed up by dozens of national and international workshops, such as JELIA, CALCULEMUS, the Induction Workshops, PROOF.PRESENTATION, USER INTERFACES for ATP; the Nonmonotonic Reasoning Workshops, the Knowledge Representation Conferences, the Frame Problem meetings and many more.
A similar growth of meetings has been seen in the other areas mentioned before, for example logic programming with its main international conferences and workshops (more than two dozen regular meetings and events). Expansion and diversity can also be found in linguistics and natural language processing with their many conferences and workshops, as well as logic and the philosophy of science with its world conference: Congress of Logic, Methodology and the Philosophy of Science. Logical foundations of computer science and verification has seen major growth with its traditional conference LICS, nowadays represented also by CAV (Computer Aided Verification), FM-Europe (Formal Methods) and others, each of which is again accompanied by national and international conferences, workshops and other events that reflect the growing industrial importance of these techniques.
This diversity is not necessarily disadvantageous, as every community that has evolved addresses its own important set of problems and issues, and it is clear that one group cannot address them all. However, fragmentation can carry a heavy price intellectually — as well as politically — in the wider arena of scientific activity where, unfortunately, logical investigations are often still perceived as limited in scope and value.
For these and other reasons we established an international federation — IFCoLog – which is registered as a legal entity and possibly accepted as a member society in the International Council of Science (ICSU). The members of the International Federation for Computational Logic (IFCoLog) will be the communities associated with the major conferences and logic societies, and they in turn will encompass the ten thousand or more individual members working on logic-related topics.
By Dana Scott & Jörg SiekmannSome Tags: verification, semantics, philosophy, language processing, reasoning, Software, formal methods, science, philosophy of science, Theorem Proving