IJCAR 2001 - Deadlines reminder + List of accepted papers

IJCAR 2001 - Deadlines reminder + List of accepted papers

[Peter Baumgartner]

------------------------------------------------------------

IJCAR 2001

The International Joint Conference on Automated Reasoning

http://www.dii.unisi.it/~ijcar/

------------------------------------------------------------

Contents:

  1) About IJCAR
  2) Deadlines reminder
  3) List of accepted Research Papers
  4) List of accepted System Descriptions

1) About IJCAR
--------------

The International Joint Conference on Automated Reasoning (IJCAR) is
the fusion of three major conferences in Automated Reasoning: CADE
(The International Conference on Automated Deduction), TABLEAUX (The
International Conference on Automated Reasoning with Analytic Tableaux
and Related Methods) and FTP (The International Workshop on
First-Order Theorem Proving). These three events will join for the
first time at the IJCAR conference in Siena in June 2001.


2) Deadlines reminder
---------------------

The submission deadline for research papers and system descriptions
has passed. However, submission of short papers and submission to
workshops is still open. 

  Short papers submission deadline     : April 2, 2001

  Workshop submission deadlines:

    Theory and Application of 
    Quantified Boolean Formulas        : March 24, 2001

    Verification                       : March 25, 2001

    Future directions in               
    Automated Reasoning                : March 29, 2001

    Mechanized Reasoning about 
    Languages with Variable Bindings   : March 30, 2001

    Precise Modelling and Deduction    
    for OO-Software Development        : March 31, 2001     

    Automation of Proof by 
    Mathematical Induction             : March 31, 2001

    Strategies in Automated Deduction 
    (STRATEGIES 2001)                  : March 31, 2001

    Proof Transformations, Proof 
    Presentations and Complexity 
    of Proofs (PTP-01)                 : March 31, 2001

    Issues in the Design and 
    Experimental Evaluation of Systems 
    for Modal and Temporal Logics      : April 1, 2001

    Unification (UNIF-2001)            : April 15, 2001

For details please visit the IJCAR web page given above.


3) List of accepted Research Papers
-----------------------------------

(88 submitted, 37 accepted)

Ulrike Sattler, Moshe Y. Vardi
The Hybrid mu-Calculus

Carsten Lutz
NExpTime-complete Description Logics with Concrete Domains

R. Pliuskevicius
Deduction-based Decision Procedure  for a Clausal Miniscoped Fragment of FTL

Carsten Lutz, Holger Sturm, Frank Wolter, Michael Zakharyaschev
A tableau calculus for temporal description logic: the constant domain case

Juergen Giesl, Deepak Kapur
Decidable Classes of Inductive Theorems

Arnon Avron, Iddo Lev
Canonical Propositional Gentzen-Type Systems

Aart Middeldorp, Seitaro Yuuki
Approximating Dependency Graphs using Tree Automata Techniques

Haarslev, Volker, Möller, Ralf, Turhan, Anni-Yasmin Exploiting Pseudo
Models for TBox and ABox Reasoning in Expressive Description Logics

Bernard Boigelot, Sébastien Jodogne, Pierre Wolper On the Use of Weak
Automata for Deciding Linear Arithmetic with Integer and Real
Variables

Haarslev, V., Moeller, R., Wessel, M.  The Description Logic ALCNHR
Extended with Concrete Domains: A Practically Motivated Approach

Gilles Audemard, Laurent Henocque
The eXtended Least Number Heuristic

Nicolas Peltier
A general method for using schematizations in automated deduction

Franz Baader, Stephan Tobies
The Inverse Method Implements the Automata Approach for Modal Satisfiability

Marco Benedetti
Conditional Pure Literal Graphs

CERRITO Serenella, CIALDEA-MAYER Marta Free-Variable Tableaux for
Constant-Domain Quantified Modal Logics with Rigid and Non-Rigid
Designation

Bernhard Beckert, Steffen Schlager
A Sequent Calculus for First-order Dynamic Logic with Trace Modalities

Pablo Armelin, David Pym
Bunched Logic Programming (Extended Abstract))

W. Reif, G. Schellhorn, A. Thums
Flaw Detection in Formal Specification

Stefan Szeider
NP-Completeness of Refutability by Literal-Once Resolution

Xavier Urbain Automated Incremental Termination Proofs for
Hierarchically Defined Term Rewriting Systems

Sylvie Doutre, Jerome Mengin Preferred Extensions of Argumentation
Frameworks: Query Answering and Computation

Reiner Haehnle, Neil V. Murray, Erik Rosenthal
Ordered Resolution vs. Connection Graph Resolution

Andrea Formisano, Eugenio G. Omodeo, Marco Temperini
Instructing equational set-reasoning with Otter

Martin Giese
Incremental Closure of Free Variable Tableaux

Hans de Nivelle, Ian Pratt-Hartmann A Resolution-Based Decision
Procedure for the Two-Variable fragment with Equality

Marko Luther
More On Implicit Syntax

Kewen Wang
A Top-down Procedure for Disjunctive Well-founded Semantics

Brigitte Pientka
Termination and Reduction Checking for Higher-Order Logic Programs

Enrico Giunchiglia, Massimo Maratea, Armando Tacchella, Davide Zambonin
Evaluating search heuristics and optimization techniques in
propositional satisfiability

Jürgen Stuber
A Model-based Completeness Proof of Extended Narrowing And Resolution

Joshua S. Hodas, Naoyuki Tamura LolliCoP -- A Linear Logic
Implementation of a Lean Connection-Method TheoremProver for
First-Order Classical Logic

Uwe Egly, Stephan Schmitt
Deriving Modular Programs from Short Proofs

Christopher Lynch, Barbara Morawska
Decidability and Complexity of Finitely Closable Linear Equational Theories

Uwe Waldmann Superposition and Chaining for Totally Ordered Divisible
Abelian Groups(Extended Abstract)

Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov
On the Evaluation of Indexing Techniques for Theorem Proving

Harald Ganzinger, David McAllester
Bottum-up deduction with deletion

Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
Context trees


4) List of accepted System Descriptions
---------------------------------------
(24 submitted, 19 accepted)

Maria Paola Bonacina
Combination of distributed search and multi-search in Peers-mcd.d

Dominique PASTRE
Muscadet 2.3: A Knowledge-based Theorem Prover Based on Natural Deduction

Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Alexey Nogin JProver:
Integrating Connection-based Theorem Proving into Interactive Proof
Assistants

Michael Beeson
A Second-order Theorem Prover applied to Circumscription

Peter F. Patel-Schneider, Roberto Sebastiani
A System and Methodology for Generating Random Modal Formulae

Haarslev, V., Moeller, R.
RACE System Description

C. Anger, K. Konczak, Th. Linke
NoMoRe: A System for NonMonotonic Reasoning with logic Programs under
Answer Set Semantic

Jens Happe
The ModProf Theorem Prover

Stephan Schulz
System Abstract: E 0.61

Alessandro Armando, Luca Compagna, Silvio Ranise
System Description: RDL---Rewrite and Decision procedure Laboratory

Kahlil Hodgson, John Slaney
Development of a Semantically Guided Theorem Prover

Armin Fiedler
P.rex: An Interactive Proof Explainer

Reinhold Letz, Gernot Stenz
DCTP -- A Disconnection Calculus Theorem Prover -- System Abstract

D. Larchey-Wendling, D. Mery, D. Galmiche
STRIP: Structural sharing for efficient proof-search

Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella
QuBE: A system for deciding Quantified Boolean Formulas Satisfiability

Joerg Luecke
Hilberticus - a Tool Deciding an Elementary Sublanguage of Set Theory

Farinas del Cerro, Luis, Fauthoux, David, Gasquet, Olivier, Herzig,
Andreas, Longin, Dominique, Massacci, Fabio Lotrec: The Generic
Tableau Prover for Modal and Description Logics

Jürgen Avenhaus, Bernd Löchner
CCE: Testing Ground Joinability

Alexandre Riazanov, Andrei Voronkov
Vampire 1.1 (system description)

-- 
Peter Baumgartner           Tel. (Giessen): +49 641 99-32160      
Mail: peter@uni-koblenz.de  Tel. (Koblenz): +49 261 287-2777    
 WWW: http://www.informatik.uni-giessen.de/staff/baumgart/