AARNEWS - October 2001



No. 53, October 2001


From the AAR Presidnet
Results of the CADE Trustee Elections 2001

A Strategy for Proving Theorems in Many-Valued Logic

Abstract of Ph.D. Thesis


Call for Papers
  • Call for Workshops and Tutorials
  • Call for Papers

  • LICS 2002
  • CAV'02
  • RTA 2002
  • FME2002
  • TABLEAUX 2002
  • From the AAR President, Larry Wos...

    Developing methods and software to help mathematicians, scientists, and engineers with the deductive aspects of their work -- this has long been and remains one of the goals of automated reasoning. I am pleased, therefore, to note that in this issue of the AAR Newsletter, we have two contributions that accomplish that goal. One contribution, by Robert Veroff, focuses on proving theorems in many-valued logic; the second contribution, by Armando Tacchella, focuses on the design and implementation of procedures for automated deduction in propositional and other logics. Both contributions report real success: in proving challenging theorems and in verifying real hardware designs.

    Results of the CADE Trustee Elections 2001

    Maria Paola Bonacina
    (Secretary of AAR and CADE)
    E-mail: bonacina@cs.uiowa.edu

    An election was held from August 30 through September 15 to fill three positions on the board of trustees of CADE Inc. Two positions were left vacant by Claude Kirchner and Frank Pfenning, whose terms expired, and a third one was created to continue the implementation of the amendment approved in the summer of 2000 to increase the number of trustees from nine to twelve (see AAR Newsletters No. 48, August 2000, and No. 52, August 2001). Gilles Dowek, Bernhard Gramlich, John Harrison and Frank Pfenning were nominated for these positions.

    Ballots were sent by electronic mail to all members of AAR as of August 30, for a total of 548 ballots (up from 445 in 2000 and 396 in 1999). Of these, 123 were returned with a vote, representing a participation level of 22.5% (down from 24.5% in 2000 and 30% in 1999). The majority is 50% of the votes plus 1, hence 62.

    The following table reports the initial distribution of preferences among the four candidates:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. Total
    G. Dowek 23 35 28 37 123
    B. Gramlich 20 23 28 52 123
    J. Harrison 43 21 31 28 123
    F. Pfenning 37 41 20 25 123

    No candidate reaches a majority right away, and the redistribution of the votes of Bernhard Gramlich yields the following new distribution:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. Total
    G. Dowek 34 35 45 9 123
    J. Harrison 48 29 42 4 123
    F. Pfenning 41 52 28 2 123

    Again, no candidate reaches a majority, and by redistributing the votes of Gilles Dowek one gets the following table:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. Total
    J. Harrison 60 59 3 1 123
    F. Pfenning 61 58 2 2 123

    Thus, Frank Pfenning, current vice-president of CADE Inc., is re-elected for a second term on the board of trustees. (Since 61 is one vote short of the majority, the STV algorithm executes another round distributing the votes of John Harrison, but this is not reported because the outcome is obvious.) The redistribution of the votes of the winner produces the following table:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. Total
    G. Dowek 39 43 37 4 123
    B. Gramlich 29 34 58 2 123
    J. Harrison 54 34 33 2 123

    None of the candidates has a majority to be elected, so that the votes of Bernhard Gramlich need to be redistributed again:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. Total
    G. Dowek 57 55 9 2 123
    J. Harrison 65 52 6 0 123

    Thus, John Harrison has a majority and is elected. Returning to the table after Frank Pfenning's votes were redistributed, and redistributing those of John Harrison also, one obtains the following matrix:

    Candidate 1st Pref. 2nd Pref. 3rd Pref. 4th Pref. Total
    G. Dowek 64 54 5 0 123
    B. Gramlich 50 67 6 0 123

    so that Gilles Dowek has a majority and is elected.

    After this election, the following people are serving on the board of trustees of CADE Inc.:

    Maria Paola Bonacina (Secretary)
    Gilles Dowek (Elected 9/2001)
    Ulrich Furbach (President, elected 8/1997 and re-elected 10/2000)
    Harald Ganzinger (Past program chair, elected 10/1999)
    John Harrison (Elected 9/2001)
    Michael Kohlhase (Elected 10/2000)
    David McAllester (Past program chair, elected 10/2000)
    Neil V. Murray (Treasurer)
    Frank Pfenning (Vice-President, elected 10/1998 and re-elected 9/2001)
    David A. Plaisted (Elected 10/1999)
    Andrei Voronkov (Program Chair of CADE 2002)

    On behalf of the AAR and CADE Inc., I thank Claude Kirchner, for his service as trustee during the past three years, Tobias Nipkow, for his service as program co-chair of IJCAR 2001 and ex-officio trustee, Bernhard Gramlich, for running in the election, all the members who voted, for their participation, and offer the warmest congratulations to Frank Pfenning, John Harrison and Gilles Dowek on being elected.

    A Strategy for Proving Theorems in Many-Valued Logic

    Robert Veroff
    E-mail: veroff@cs.unm.edu

    In this note, we outline a strategy that has worked quite well on a number of challenging problems in many-valued logic. The strategy is based on the use of proof sketches, first presented in [3].


    This work concerns the application of automated reasoning to logical systems based on the inference rule condensed detachment (CD). CD, which is a combination of modus ponens and universal instantiation, can be implemented in an automated reasoning system such as OTTER [1] by using hyperresolution and the following clause.

       -P(i(x,y)) | -P(x) | P(y).

    Many-valued logic (MV) can be defined (in clause form) with the following five axioms.1

       P(i(x,i(y,x)))                  # label("MV1").
       P(i(i(x,y),i(i(y,z),i(x,z))))   # label("MV2").
       P(i(i(i(x,y),y),i(i(y,x),x)))   # label("MV3").
       P(i(i(n(x),n(y)),i(y,x)))       # label("MV4").
       P(i(i(i(x,y),i(y,x)),i(y,x)))   # label("MV5").

    MV is a sublogic of two-valued logic (TV) in the sense that each of the axioms of MV is a theorem of TV. The Lukasiewicz system

       P(i(i(x,y),i(i(y,z),i(x,z))))   # label("L1").
       P(i(i(n(x),x),x))               # label("L2").
       P(i(x,i(n(x),y)))               # label("L3").

    is one of several equivalent axiomatizations of TV. We exploit the relationship between MV and TV as part of our strategy.

    The strategy described in this note relies on the generation and use of proof sketches, sets of clauses containing potentially key milestones on the way to a proof of a target theorem T. Operationally, the clauses appearing in a proof sketch are used as hints [2] to help guide the search for a proof of T. In particular, we put a bias in our search toward deduced clauses that back subsume such hint clauses.

    We are especially interested in developing strategies for finding proof sketches that effectively lead to the proofs of target theorems. For example, one approach is to prove the target theorem with additional assumptions and then systematically eliminate these assumptions--using previous proofs as proof sketches--until a proper proof of the theorem is found.

    Example Problems Solved

    We recently have proved the following four distributivity theorems in MV,

       % KA1: K distributes over A, direction 1 (KpAqr -> AKpqKpr)
       % KA2: K distributes over A, direction 2 (KpAqr <- AKpqKpr)
       % AK1: A distributes over K, direction 1 (ApKqr -> KApqApr)
       % AK2: A distributes over K, direction 2 (ApKqr <- KApqApr)

    and the following theorem in the implicational fragment of MV.

       % HR: single axiom

    The implicational fragment of MV (MVI) is the sublogic defined by the axioms {MV1, MV2, MV3, MV5}. HR is known to be a single axiom for MVI, but in this note we are concerned only with showing that it is a theorem.

    The comments preceding the distributivity theorems refer to operators A and K. These operators are related, respectively, to our usual notions of logical disjunction (or) and conjunction (and) and are defined as follows.

    A(x,y) = i(i(x,y),y)
    K(x,y) = n(i(i(n(x),n(y)),n(y)))

    You can read more about these theorems and see their proofs on the Web.

    The significance of these theorems for this short note is simply that they appear to be especially difficult to prove with OTTER. One reason is that they are fairly long formulas when compared with the lengths of the axioms; the HR single axiom, for example, has length 70. OTTER tends to work better when its search can be restricted to shorter formulas.

    A Strategy

    Here is a rough outline of a strategy for proving a theorem T in many-valued logic (or in some related logic). The basic idea is that the proof or proofs found for each step can be used as proof sketches to help guide the search in the later steps. We note that some of these steps are nontrivial and present interesting challenges themselves. We will discuss some of these issues in more detail in a future article.

    Each step i results in a proof (or set of proofs), which we will denote Proofi.

    1. Prove T in two-valued logic (TV).

      Finding a proof in TV often is substantially easier than finding a proof in MV. Although a proof in TV is not necessarily a proof in MV, given the close tie between the two logics, the TV proof may tell us a lot about what to look for in an MV proof, for example, if it contains steps that are theorems in MV.

      Finding a TV proof may involve using several of the techniques described in [3], for example, relying on heuristics that include the use of paramodulation and demodulation and permitting applications of inferences rules to the clause representing the denial of the theorem and to its descendants.

      Although there are known substitution properties for TV, at this point we may relax things even further by permitting in addition certain paramodulation steps that may not be sound even in TV. For example, we may permit paramodulations from clauses of the form


      when P(i(t1,t2)) is known to be a theorem, even though P(i(t2,t1)) may not be a theorem. As a consequence, Proof1 may contain steps that are not theorems in TV. Nevertheless, finding such a proof has proven to be a useful starting point for our searches.

    2. Eliminate demodulation from the previous proof by replacing each application of demodulation with a corresponding application of paramodulation.

      We use OTTER to find this proof by including all of the intermediate demodulants used in Proof1 as hints for this step.

    3. Get a strictly forward demodulation-free derivation.

      We use OTTER to find this proof by including the positive form of every negative clause appearing in Proof2. For example, if -P(i(a,i(b,a)) appears in Proof2, we include P(i(x,i(y,x)) as a hint here.

    4. Get a strictly hyperresolution proof by including clauses of the form

         -P(i(x,y)) | -P(i(y,x)) | P(t[x],t[y]).

      where t[x] is a term with exactly one occurrence of the variable symbol x, and t[y] is the same term but with variable symbol y instead of x. Note that a hyperresolvent resulting from such a clause characterizes a type of substitution property when used as the major premise in an application of CD. We'll refer to such a clause as a substitution theorem.

      Although it may appear that a sufficient set of substitution theorems can be determined directly from the paramodulation steps in Proof3, this is not necessarily the case, depending, for example, on the types of inference steps permitted in Proof1.

    5. Assuming the relevant "lemmas" P(i(x,y)) and P(i(y,x)), find a derivation for each of the substitution theorems used in Proof4.

      Although we could implement a special procedure for this step, we have been successful at using OTTER to find these derivations.

    6. Find a CD derivation of T from the axioms of MV (or MVI). That is, using the accumulation of proof sketches for guidance, we attempt to prove the original theorem in the original logic.

    As we indicated, some of these individual steps can be challenging. It took us several weeks to find the proof of theorem KA2, and the proof we found is 140 steps long. On the other hand, we found a CD derivation of theorem HR two days after we were presented the problem.


    1. MV5 is known to be dependent on {MV1, MV2, MV3, MV4}.


    McCune, W.: 1994, OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois.

    Veroff, R.: 1996, "Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies," J. Automated Reasoning, 16(3), 223-239.

    Veroff, R.: 2001, "Solving Open Questions and Other Challenge Problems Using Proof Sketches," J. Automated Reasoning, 27(2), 157-174.

    Abstracts of Recent Ph.D. Theses in Automated Reasoning

    Title: SAT-based Decision Procedures for Knowledge Representation and Formal Verification

    Author: Armando Tacchella

    Advisor: Proff. Enrico Giunchiglia and Mauro Di Manzo

    Defense date: February 2001

    Institution: Dipartimento di Informatica, Sistemistica e Telematica, Università degli Studi di Genova, Italia

    Abstract: This work focuses on the development of computer procedures for automated deduction in the following logics:

    • propositional logic (or Boolean logic) and the related satisfiability problem, i.e., establishing whether a given a sentence in propositional logic is contradictory or not;
    • modal logics, i.e., the extension of propositional logic to deal with modalities such as time and knowledge;
    • quantified propositional logic, i.e., the extension of propositional logic to deal with quantifications
    The choice of the above logics was mainly dictated by the fact that several problems of interest in the fields of knowledge representation and formal verification can be naturally encoded using propositional logic, or its modal and quantified superclasses.

    The contribution of this thesis is the design, the implementation and the experimental testing of three systems:

    • SIM (Satisfiability Internal Modules), a library of efficient decision procedures based on the Davis-Putnam-Logemann-Loveland (DPLL) method for propositional satisfiability.
    • *SAT (Everything on SAT), a platform for the development of SAT-based, and particularly, DPLL-based decision procedures for various modal logics.
    • QuBE (Quantified Boolean formulas Evaluator), a collection of decision procedures for quantified Boolean logic.
    Each system embeds both state-of-the-art techniques, and new ideas and algorithms that were developed in the course of the thesis to improve on the current available decision procedures in all the logics that we review. As a result, SIM, *SAT and QuBE compare favorably with analogous systems from other researchers, and particularly:
    • SIM compares favorably with the systems presented in [BS97, Zha97, LA97, Fre95] and it can outperform them using the same techniques they use, but combining them to foster effectiveness;
    • *SAT is continuously under development; the current version 3.2 embeds SATO [Zha97a] as the internal DPLL solver and it compared well with the systems presented in [PS98, Hor97, HS97]; we are currently developing a new version which will include SIM as the internal solver and will be able to handle expressive modal logics.
    • QuBE is faster than other comparable state-of-the-art systems (such as the one presented in [CGS98]) and it features some newly introduced technique as well.

    The systems that we developed are interesting not only from the research perspective, but also from an application point of view. SIM is at the heart of two technology-transfer projects. The first one is THUNDER, an open architecture for SAT-based verification of hardware designs developed by the Logic Validation Technologies Group at the Israel Development Center of Intel Corp. An object oriented version of SIM (SIMO) has been recently integrated into THUNDER and used to debug the design of some Pentium IV components. THUNDER(SIMO) outperforms other traditional validation technologies [CF+01]. The second technology transfer project centered around SIM is in cooperation with Istituto per la Ricerca Scientifica e Tecnologica (IRST-ITC) in Trento and involves the integration of SIM into the NuSMV [CC+98] model checker, a tool for debugging and verifying hardware designs and software protocols.

    On-line resources
    SIM and QuBE homepages under Software Tools for Automated Reasoning (STAR) pages.
    *SAT homepage, including source code distribution, manual, papers and more.

    [BS97] R. J. Bayardo Jr. and R. C. Schrag. Using CSP Look-Back Techniques to Solve Real-World SAT instances. In Proc. of AAAI, pages 203-208. AAAI Press, 1997.
    [CC+98] A. Cimatti, E. Clarke, F. Giunchiglia and M. Roveri. NuSMV: A new symbolic model checker. Journal on Software Tools for Technology Transfer, 2:4, pages 410-425, Springer Verlag, 2000.
    [CF+01] F. Copty, L. Fix, Ranan Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella and M. Y. Vardi. Benefits of bounded model checking at an industrial setting. In Proc. of CAV, 2001.
    [CGS98] M. Cadoli, A. Giovanardi, and M. Schaerf. An algorithm to evaluate quantified boolean formulae. In Proc. of AAAI, 1998.
    [Fre95] J. W. Freeman. Improvements to propositional satisfiability search algorithms. Ph.D. thesis, University of Pennsylvania, 1995 .
    [Hor97] I. Horrocks. Optimizing tableaux decision procedures for description logics. Ph.D. thesis, University of Manchester, 1997.
    [HS97] U. Hustadt and R. A. Schmidt. On evaluating decision procedures for modal logic. In Proc. of IJCAI, 1997.
    [LA97] C. M. Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proc. of IJCAI, pages 366--371. Morgan-Kauffmann, 1997.
    [PS98] P. F. Patel-Schneider. DLP system description. In Collected Papers from the International Description Logics Workshop (DL'98). CEUR Workshop Proceedings, 1998.
    [Zha97] H. Zhang. SATO: An efficient propositional prover. In Proc. of CADE, volume 1249 of LNAI, pages 272--275. Springer Verlag, 1997.

    CADE-18 News

    CADE-18 Call for Papers

    The Conference on Automated Deduction (CADE) is the major international forum at which research on all aspects of automated deduction is presented. The first conference was held in 1974. Early CADEs were mostly biennial; annual conferences have been held since 1996. In 2001, CADE, TABLEAUX, and FTP merged into one conference called the International Joint Conference on Automated Reasoning (IJCAR). This year CADE-18 is a participant of the Federated Logic Conference (FLoC'02), which will be held in Copenhagen, Denmark, July 27-30, 2002.

    CADE-18 invites submissions related to all aspects of automated deduction, including foundations, implementations, and applications. Original research papers and descriptions of working automated deduction systems are solicited.

    Logics of interest include propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many-valued, substructural, description, and meta-logics, type theory and set theory.

    Techniques of interest include induction, term rewriting, constraint solving, satisfiability checking, model checking, resolution, semantic tableaux, sequent calculi, model-elimination, inverse method, interactive theorem proving, proof planning, term indexing, implementation techniques, decision procedures, unification, model generation, semantic guidance, logical frameworks, proof presentation.

    Applications of interest include verification, formal methods, program analysis and synthesis, declarative programming, proof carrying code, deductive databases, knowledge representation, computer mathematics, natural language processing, linguistics, robotics, planning.

    There are three categories of submission: (A) regular papers (max. 15 pages), (B) experimental papers (max. 10 pages), and (C) system descriptions (max. 5 pages) accompanied by a demonstration. The proceedings of CADE-18 will be published by Springer-Verlag in the LNAI/LNCS series. All submissions must be received by February 2, 2002. Details about paper preparation are in the Web site. Details about CADE-18 are available on the Web site.

    As in previous CADEs, an Automated Theorem Prover System Competition will be held at CADE-18.

    CADE-18 Call for Workshops and Tutorials

    The 18th International Conference on Automated Deduction will take place in Copenhagen, Denmark, on July 27-30, 2002. Workshops and tutorial will be held July 25, 26, and 31 and August 1, 2002.

    Workshops and tutorials will ordinarily run for one or two days, but half-day ones may be possible as well.

    Workshop Topics. Recent CADE workshops have included term schematizations and their applications, reasoning, automation of proofs by induction, empirical studies in logic algorithms, mechanizations of partial functions, proof search in type-theoretic languages, automated model building, evaluation of automated theorem-proving systems, strategies in automated deduction, automated theorem proving in software engineering and in mathematics, and integration of symbolic computation and deduction. We encourage workshops that build on previous events as well as new ones in novel research areas broadly related to automation and deduction.

    Tutorial Topics. Recent CADE tutorials have included equality reasoning in semantic tableaux, proof systems for nonmonotonic logics, rewrite techniques in theorem proving, proof planning, parallelisation of deduction strategies, resolution decision methods, constructive type theory, the use of semantics in Herbrand-based proof procedures, logical frameworks, theorem proving by the inverse method, deduction methods based on boolean rings, higher-order equational logic, and term indexing in automated reasoning. Tutorials may be introductory, intermediate, or advanced. Tutorials on novel research are also encouraged.

    Proposals. Anyone wishing to organize a workshop or tutorial in conjunction with CADE-18 should send (e-mail preferred) a proposal (in ASCII text format) no longer than two pages to the workshop/tutorial chair and the program chair by October 12, 2001. The proposal should describe the following:

  • the title of the workshop or tutorial,
  • the names and affiliations of person or persons who will chair the workshop or present the tutorial,
  • a brief technical description of the topic of the workshop or tutorial,
  • contact details (email, web page, phone, fax, etc.),
  • a list of workshops or tutorials previously organised or given in this or related areas,
  • the preferred date for the workshop or tutorial (pre-CADE, post-CADE or any),
  • the proposed duration of workshop or tutorial (1 day, 2 days),
  • invited speakers, and
  • plans to have proceedings or other publications of the workshop or tutorial.
  • Proposals will be evaluated, and decisions will be communicated by October 26, 2001. Further information about the arrangements for workshops and tutorials can be obtained from the CADE-18 Web site.

    Call for Papers

    LICS 2002

    The seventeenth annual IEEE Symposium on Logic in Computer Science will take place on July 22-25, 2002, in Copenhagen, Denmark, as part of the 2002 Federated Logic Conference (FLoC 2002).

    Topics of interest for submissions include automated deduction, categorical models and logics, constraint programming, database theory, domain theory, finite model theory, formal aspects of program analysis, formal methods, lambda and combinatory calculi, linear logic, logics in artificial intelligence, logics of programs, logic programming, modal and temporal logics, model checking, programming language semantics, reasoning about security, rewriting, type systems and type theory, and verification.

    The deadline for submissions is January 15, 2002. For further information, see the Web site.

    LICS 2002 will have a session of short (5-10 minutes) presentations. This session is intended for descriptions of work in progress, student projects, and relevant research being published elsewhere; other brief communications may be acceptable. Submissions for these presentations, in the form of short abstracts (1 or 2 pages), should be entered at the LICS submission site March 25-29, 2002.

    Kleene Award for Best Student Paper: An award in honor of the late S. C. Kleene will be given for the best student paper, as judged by the program committee. For a paper to be eligible, the research presented must have been carried out while at least one of the authors was a full-time student. Multiple-authored papers are permitted. The exact circumstances, including allocation of credit, should be detailed in the submission letter, SIGNED BY ALL AUTHORS. The program committee may decline to make the award or may split it among several papers.

    Other events: The following conferences will participate at FLoC 2002: CADE, CAV, FME, ICLP, RTA, TABLEAUX; see the Web site for details. There will also be many workshops sponsored by the FLoC conferences. For details about the LICS workshops, see the Web site.


    The 14th International Conference on Computer Aided Verification (CAV'02) will be held in Copenhagen, Denmark, on July 27-31, 2002. This year's CAV conference will be part of the Federation of Logic Conferences. Topics of interest include the following:

    The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series.

    There are two categories of submissions: (A) regular papers (max. 13 pages); and (B) tool presentations (max. 4 pages). Paper submissions are due January 15, 2002. For further details, see the conference home page.

    RTA 2002

    The conference on Rewriting Techniques and Applications (RTA 2002) will be held on July 22-24, 2002, in Copenhagen, Denmark, as part of the Federated Logic Conference FLoC'02.

    RTA 2002 solicits original papers on all aspects of rewriting, including applications, foundations, frameworks, implementations, semantics. There are four submission categories: (1) regular research papers describing new results, (2) papers describing the experience of applying rewriting techniques in other areas, (3) problem sets that provide realistic and interesting challenges in the field of rewriting, and (4) system descriptions. Submissions must reach the program chairperson by January 15, 2002. Please see the Web site for further information.


    Formal Methods Europe (FME 2002) will be held on July 20-24, 2002, in conjunction with the third Federated Logic Conference (FLoC'02) in Copenhagen, Denmark.

    The theme of FME 2002 is Formal Methods: Getting IT Right. The double meaning is intentional. On the one hand, the theme acknowledges the significant contribution formal methods can make to Information Technology, by enabling computer systems to be described precisely and reasoned about with rigour. On the other hand, it recognises that current formal methods are not perfect, and further research and practice are required to improve their foundations, applicability and effectiveness.

    FME seeks papers in all aspects of formal methods for computer systems, including the following: theoretical foundations, practical use and case studies, specification and modeling techniques, software development and refinement, tool support and software engineering environments for formal methods, verification and validation, hidden formal methods, and making benefits available to nonexperts, reusable domain theories, method integration, and hardware verification. Full papers (max. 20 pages) should be reach the Program Co-chairs by January 15, 2002.

    Tutorials and workshops will be held on 20-21 July 2002. Each tutorial will last one-half or one day. Proposals are welcome and should be directed to the Program Co-chairs by January 15, 2002.

    Tool demonstrations will also take place during the symposium, with the opportunity for presentations to be made about each tool. Proposals for tool demonstrations should be made to the Tool Demonstration Coordinator, with whom provison of necessary computing facilities should be discussed.

    For details, please see the Web site.

    TABLEAUX 2002

    A conference on Automated Reasoning with Analytic Tableaux and Related Methods will be held July 30-August 1, 2002, at Copenhagen, Denmark (in the frame of FLoC 2002). The conference brings together researchers interested in all aspects of the mechanization of reasoning with analytic tableaux and related methods.

    Topics of particular interest include analytic tableaux for various logics (theory and applications); related techniques and concepts (e.g., model checking, BDDs); related methods (model elimination, sequent calculi, connection method, inverse method, etc.); new calculi and deduction methods in classical and nonclassical logics (description, modal, intuitionistic, linear, temporal, etc.); and systems, tools, implementations and applications (e.g., verification).

    Submissions are invited in the following categories: (A) full papers (experimental or theoretical research; up to 15 pages); (B) system descriptions (up to 5 pages); and (C) position papers and reports on work in progress (up to 15 pages). Accepted papers of categories (A) and (B) will be published in Springer's LNAI series. The proceedings will be available at the conference. Accepted papers of category (C) will be available as a technical report of the Vienna University of Technology and on the Internet.

    Submissions are due February 2, 2002. For further information, please see the Web site.

    Gail Pieper