------------------------------------------------------------ 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/