Author: Reiner Hahnle
On the theoretical side the activities in this working group will aim at a better understanding of the computational properties of many-valued logics including in particular investigations into normal forms, extensions of the logic programming paradigm and approximation of infinite-valued logics by finite-valued logics.
Results from these activities will be incorporated into existing inference systems or taken into account in the development of new deductive systems.
In all the areas mentioned in the previous section, considerable scientific progress was made. This is documented in detail in the reports of the individual research teams. Moreover, a number of workshops were organized and several persistent collaborations were established. This is detailed below.
I also want to stress that several software systems were built or improved as part of the WG activities. The software is available to the public, again, details are given below.
The group managed to attract and to integrate young researchers to a considerable degree. At least four PhD theses within the area of WG 2 were finished during the runtime of the action, about six more are still running and partially owe their topics to the work discussed here.
It should be emphasized that each workshop consisted not only of scientific talks and progress reports, but was supplemented by round table and panel discussions, group work, and presentation of PhD projects. The workshops succeeded to integrate participating teams and, in particular, young researchers to a high degree.
In addition to the regular WG meetings supported by the COST framework, WG 2 was also actively involved in number of international events, thereby enhancing the visibility of COST Action:
Several of the research teams developed software that is available to interested parties through the given URLs or by contacting the individual research teams:
U of Karlsruhe: 3TAP, a generic automated theorem prover for sorted, finite-valued first-order logics, see http://www.ira.uka.de The system was applied to problems from hardware and software verification.
TU of Vienna: MUltlog is a system which takes as input the specification of a finite-valued first-order logic and produces a sequent calculus, a natural deduction system, and clause formation rules for this logic. All generated rules are optimized wrt their branching degree. The output is in the form of a scientific paper written in LaTeX, see http://www.logic.at/multlog.
U of Lleida: Both, a generalized Davis-Putnam-Loveland procedure and local search procedures were implemented for propositional satisfiability checking of many-valued (signed) clause logic. These are successfully applied to solve hard combinatorial problems. Contact: felip@eup.udl.es
MPII Saarbrucken Experiments in lattice-valued logics based on the classical automated theorem prover SPASS by translation. Contact: sofronie@mpi-sb.mpg.de.
U of Malaga: A system for simplification and validity checking of finite-valued signed logic based on a novel deduction method called TAS was developed. Contact: aciego@ctima.uma.es
Software developers benefited considerably from exchanging theoretical and practical insights during frequent contacts made possible by the COST framework.
The present author together with G. Escalada-Imaz (IIIA Barcelona) edited a Special Issue on Deduction in Many-Valued Logics of Mathware & Soft Computing. The present author edited a Special Issue on COST Action#15 of Soft Computing. D. Mundici (U of Milan) edited a Special Issue on Many-Valued Logics of Studia Logica.
WG'2 members contributed actively to each of these special issues of international journals.
Here is a list of teams together with the topics worked on within WG 2 (most teams were involved in other WG's and topics as well).
IIIA Barcelona: Gonzalo Escalada-Imaz. Topics: fuzzy logic programming, simplification.
U of Dortmund: Stephan Lehmke, Helmuth Thiele. Topics: fuzzy logic, Lukasiewicz logic.
U of Ghent: Albert Hoogewijs, Noemie Slaats. Topics: software specification.
U of Giessen: Thomas \Lukasiewicz. Topics: Probabilistic and many-valued logic programming.
U of Karlsruhe: Bernhard Beckert, Reiner H\"ahnle, Peter Schmitt. Topics: signed logic, theorem proving, simplification, software verification.
Kings College London: Hans-Jürgen Ohlbach, Dov Gabbay. Topics: labelled systems, description logics.
U of Liege: Pascal Gribomont. Topics: software verification.
U of Lleida: Ramon Bejar, Felip Manya. Topics: signed logic, satisfiability checking.
U of Malaga: Gabriel Aguilera, Inmaculada Perez de Guzman, Manuel Ojeda Aciego. Topics: signed logic, theorem proving, simplification.
MPII Saarbrucken: Viorica Sofronie-Stokkermans. Topics: signed logic based on algebras, theorem proving.
U of P.J. Safarik/Kosice: Peter Vojtas. Topics: fuzzy logic programming.
Us of Milan & Torino: Stefano Aguzzoli, Agata Ciabattoni, Ferdinando Cicalese, Daniele Mundici, Nicola Olivetti. Topics: Lukasiewicz logic, in particular normalization problems.
TU of Vienna: Matthias Baaz, Christian Fermuller, Georg Moser, Gernot Salzer, Helmuth Veith. Topics: signed logic, Godel logic, normalization, proof theory.
Institute of Telecomm. & U of Warsaw: Beata Konikowska, Ewa Orlowska. Topics: relational proof systems.
Several fruitful and persistent bilateral collaborations were established thanks to COST Action #15.
In some cases these are formally funded within bilateral national programs. Formal collaborations exist, for example, between U of Karlsruhe and IIIA Barcelona, between TU of Vienna and U of Milan, and between Kings College London and U of Karlsruhe, to name just a few.
We refer to the individual team reports for the large number of scientific papers jointly written by members of teams from different countries.
Thanks to the possibility of having invited speakers at COST meetings, the working group benefited from contacts to leading authorities living outside of Europe. This led, for example to a formal project between U of Karlsruhe and U of Campinas, Brazil.
The coordinator of WG 2 serves as well in the Technical Committee for Multiple-Valued Logic of the IEEE Computer Society and provided contacts between both groups.
The objective of this working group is to point out the general features of many-valued logics as a tool for the representation and processing of uncertain information. Reasoning under incomplete knowledge is an important issue in Artificial Intelligence nowadays.
Many-valued calculi are often encountered in the proposed approaches. For instance, possibility theory and possibilistic logic provide a natural framework for manipulating orderings between preferred interpretations, or more or less entrenched propositions in non-monotonic reasoning. Still another example is given by conditional objects which are symbolic counterparts of conditional probabilities and are 3-valued logical entities. Direct connections can be established between 3-valued logics of conditional objects and non-monotonic consequence relationships as studied by Lehmann and Magidor. Besides, truth-functional fuzzy logic has proved to be useful for modelling interpolative reasoning, as used in fuzzy control applications for instance.
These works will constitute the prerequisite theoretical foundations of the development of tools for processing and manipulating incomplete and uncertain knowledge.
Potential applications of this working group are numerous. Amongst those developed by the teams participating in the action one can cite: software synthesis, non-terminating behaviour in software verification, user-oriented inference tools, robotic planning, intelligent user interfaces, reasoning about information processing machines, etc. In the medical domain, diagnosis help will be investigated and a system devoted to the rehabilitation of aphasics will be developed.