Contents

1. International Conference TABLEAUX 2003

2. Unif '03"

International Conference TABLEAUX 2003
(Automated Reasoning with Analytic Tableaux and Related Methods)
Rome, Italy, September 9-12, 2003
Regimantas Pliuskevicius
Institute of Mathematics and Informatics
Akademijos 4, Vilnius 2600, LITHUANIA
email: regis@ktl.mii.l

The International Conference TABLEAUX 2003  (http://tab2003.dia.uniroma3.it) is a continuation of annual international meetings on Automated Reasoning with Analytic Tableaux and Related Methods held since 1992. TABLEAUX 2003 was co-located with the International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003) and the 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2003). The three events run in parallel provided the opportunity for contacts with a broader community, corroborated by the joint panel discussion and the talk by Thierry Coquand (Goteborg University, Sweden), jointly invited by Calculemus 2003 and TABLEAUX 2003. The talk "Reasoning about proof search specification" by Dale Miller (INRIA, France), invited by TPHOL, should be mentioned too.

Conference TABLEAUX 2003 brought together researchers and practitioners working on both theoretical and practical aspects of the mechanization of reasoning with tableaux and related methods. Tableaux and related methods such as Gentzen calculi are a convenient and effective formalism for automating deduction not only in classical logic but also in various non-standard logics. Results presented in conference include theoretical foundations, implementation techniques, system development for classical, modal, temporal, intuitionistic, non-monotone, conditional, paraconsistent, many-valued, intermediate and description logics. Areas of application of these investigations include verification of software and computer systems, deductive databases, knowledge representation and its required inference engines, and system diagnosis.

The technical program of the conference consisted of 3 invited talks, 14 regular papers, 3 tutorials, 8 position papers and 6 system descriptions. The regular papers and system descriptions presented at the conference were published in the Lecture Notes in Artificial Intelligence (LNAI), vol. 2796, 2003. Position papers and tutorials were published by ARACNE Editrice S.R.L. (Italy), as Technical Report RT-DIA-80-2003, Dipartimento di Informatica
e Automazione, Università degli Studi di Roma Tre.

Let us review the invited talks presented at TABLEAUX 2003. J.Schumann (NASA Ames Research Center, USA) presented interesting talk "Automated theorem proving in generation, verification, and certification of safety critical code". In this talk J.Schumann reported on automatic program synthesis systems for state estimation and navigation, AUTOFILTER, and data analysis, AUTOBAYES. These tools automatically generate documented C/C++ code from high-level specifications written in compact domain-specific language. Program synthesis systems are based on some logical inference mechanism, graph reasoning, symbolic algebra and rewriting techniques. For safety-critical applications, the generated code must be certified. It is required the code producer to provide formal proofs that the code satisfies certain safety properties. The system generates some verification conditions which are processed by automatic theorem prover e-SETHEO. M.Abrusci (Rome University, Italy) presented talk "Non commutative logic: A survey". Non commutative logic (NL) has been introduced by Abrusci and Ruet in 2001. NL is a refinement of Girard's Linear Logic and a conservative extension of Lambek Calculus. NL allows to deal with commutative and non commutative conjunctions and disjunctions. The talk surveys the main results obtained in NL by several authors during 2001-2003, concerning proof-nets, sequent calculus, proof search, completeness theorem and others.
T. Coquand (Goteborg University, Sweden) presented talk "Dynamical method in algebra: A survey". In this talk T.Coquand presented a possible realization of Hilbert's program for some part of abstract algebra.There is a method allowing computations in the algebraic closure of a field, though it is known that such a closure may fail to exist constructively. The talk surveys some results connected with this phenomenon. In the talk the notion of "geometric logic" is presented. The proof in this logic are constructed in some informal way. In some talks presented at the TABLEAUX 2003 it was stressed that it has been developed a number of successful automated deduction systems and methods based on tableau and sequent paradigm. These systems and methods have more rich structure than resolution based systems.

In TABLEAUX 2003 I have presented position paper (with A.Pliuskeviciene) "Decision Procedure for a Fragment of FTL with Equality". As far as we know, the presented decision procedure is the first one for first-order linear temporal logic with equality. We are grateful the CoLogNET and EU contribution under the IST-FET programme for financial support that allows me to participate in the conference TABLEAUX 2003 and present these results.

UNIF'03

UNIF 2003 is the 17th in a series of annual international workshops on unification, the previous ones having been in Val D'Ajol, France (1987 and 1988), Lambrecht, Germany (1989), Leeds, England (1990), Barbizon, France (1991), Dagstuhl, Germany (1992), Boston, USA (1993), Val D'Ajol, France (1994), Sitges, Spain (1995), Herrsching, Germany (1996), Orléans, France (1997),Rome, Italy (1998), Frankfurt, Germany (1999), Pittsburgh, USA (2000), Siena, Italy (2001), and Copenhagen, Denmark (2002).

Unification is concerned with the problem of identifying given terms,either syntactically or modulo a given logical theory. The topic is understood in a rather broad sense at this workshop. The aim of UNIF 2003, as that of the previous meetings, is to to bring together people interested in unification, present recent (even unfinished) work, and discuss new ideas and trends in unification and related fields. In this edition of the workshop, the organizing committee decided to include a panel on ``Open Problems in Unification''.

A list of typical UNIF topics includes, but is not limited to: