1. IJCAR 2001: Siena, Italy

Invited Talks

• Neil D. Jones:
  Program Termination Analysis by Size-Change Graphs (Abstract). 1-4
  
• Lawrence C. Paulson:
  SET Cardholder Registration: The Secrecy Proofs. 5-12
  
• Andrei Voronkov:
  Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. 13-28
  

Description, Modal and Temporal Logics

• Volker Haarslev, Ralf Möller, Michael Wessel:
  The Description Logic ALCNH_R+ Extended with Concrete Domains: A Practically Motivated Approach. 29-44
  
• Carsten Lutz:
  NEXPTIME-Complete Description Logics with Concrete Domains. 45-60
  
• Volker Haarslev, Ralf Möller, Anni-Yasmin Turhan:
  Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics. 61-75
  
• Ulrike Sattler, Moshe Y. Vardi:
  The Hybrid µ-Calculus. 76-91
  
• Franz Baader, Stephan Tobies:
  The Inverse Method Implements the Automata Approach for Modal Satisfiability. 92-106
  
• Regimantas Pliuskevicius:
  Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL. 107-120
  
• Carsten Lutz, Holger Sturm, Frank Wolter, Michael Zakharyaschev:
  Tableaux for Temporal Description Logic with Constant Domains. 121-136
  
• Serenella Cerrito, Marta Cialdea Mayer:
  Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation. 137-151
  

Saturation Based Theorem Proving, Applications, and Data Structures

• Andrea Formisano, Eugenio G. Omodeo, Marco Temperini:
  Instructing Equational Set-Reasoning with Otter. 152-167
  
• Stefan Szeider:
  NP-Completeness of Refutability by Literal-Once Resolution. 168-181
  
• Reiner Hähnle, Neil V. Murray, Erik Rosenthal:
  Ordered Resolution vs. Connection Graph Resolution. 182-194
  
• Jürgen Stuber:
  A Model-Based Completeness Proof of Extended Narrowing and Resolution. 195-210
  
• Hans de Nivelle, Ian Pratt-Hartmann:
  A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality. 211-225
  
• Uwe Waldmann:
  Superposition and Chaining for Totally Ordered Divisible Abelian Groups. 226-241
  
• Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela:
  Context Trees. 242-256
  
• Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov:
  On the Evaluation of Indexing Techniques for Theorem Proving. 257-271
  

Logic Programming and Nonmonotonic Reasoning

• Sylvie Doutre, Jérôme Mengin:
  Preferred Extensions of Argumentation Frameworks: Query Answering and Computation. 272-288
  
• Pablo A. Armelín, David J. Pym:
  Bunched Logic Programming. 289-304
  
• Kewen Wang:
  A Top-Down Procedure for Disjunctive Well-Founded Semantics. 305-317
  
• Michael Beeson:
  A Second-Order Theorem Prover Applied to Circumscription. 318-324
  
• Christian Anger, Kathrin Konczak, Thomas Linke:
  NoMoRe : A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semantics. 325-330
  

Propositional Satisfiability and Quantified Boolean Logic

• Marco Benedetti:
  Conditional Pure Literal Graphs. 331-346
  
• Enrico Giunchiglia, Marco Maratea, Armando Tacchella, Davide Zambonin:
  Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability. 347-363
  
• Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella:
  QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. 364-369
  
• Stephan Schulz:
  System Abstract: E 0.61. 370-375
  
• Alexandre Riazanov, Andrei Voronkov:
  Vampire 1.1 (System Description). 376-380
  
• Reinhold Letz, Gernot Stenz:
  DCTP - A Disconnection Calculus Theorem Prover - System Abstract. 381-385
  

Logical Frameworks, Higher-Order Logic, Interactive Theorem Proving

• Marko Luther:
  More On Implicit Syntax. 386-400
  
• Brigitte Pientka:
  Termination and Reduction Checking for Higher-Order Logic Programs. 401-415
  
• Armin Fiedler:
  P.rex: An Interactive Proof Explainer. 416-420
  
• Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin:
  JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. 421-426
  

Semantic Guidance

• Gilles Audemard, Laurent Henocque:
  The eXtended Least Number Heuristic. 427-442
  
• Kahlil Hodgson, John K. Slaney:
  System Description: SCOTT-5. 443-447
  
• Maria Paola Bonacina:
  Combination of Distributed Search and Multi-search in Peers-mcd.d. 448-452
  
• Luis Fariñas del Cerro, David Fauthoux, Olivier Gasquet, Andreas Herzig, Dominique Longin, Fabio Massacci:
  Lotrec : The Generic Tableau Prover for Modal and Description Logics. 453-458
  
• Jens Happe:
  The MODPROF Theorem Prover. 459-463
  
• Peter F. Patel-Schneider, Roberto Sebastiani:
  A New System and Methodology for Generating Random Modal Formulae. 464-468
  

Equational Theorem Proving and Term Rewriting

• Jürgen Giesl, Deepak Kapur:
  Decidable Classes of Inductive Theorems. 469-484
  
• Xavier Urbain:
  Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems. 485-498
  
• Christopher Lynch, Barbara Morawska:
  Decidability and Complexity of Finitely Closable Linear Equational Theories. 499-513
  
• Harald Ganzinger, David A. McAllester:
  A New Meta-complexity Theorem for Bottom-Up Logic Programs. 514-528
  

Tableau, Sequent, Natural Deduction Calculi and Proof Theory

• Arnon Avron, Iddo Lev:
  Canonical Propositional Gentzen-Type Systems. 529-544
  
• Martin Giese:
  Incremental Closure of Free Variable Tableaux. 545-560
  
• Uwe Egly, Stephan Schmitt:
  Deriving Modular Programs from Short Proofs. 561-577
  
• Nicolas Peltier:
  A General Method for Using Schematizations in Automated Deduction. 578-592
  

Automata, Specification, Verification, and Logics of Programs

• Aart Middeldorp:
  Approximating Dependency Graphs Using Tree Automata Techniques. 593-610
  
• Bernard Boigelot, Sébastien Jodogne, Pierre Wolper:
  On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. 611-625
  
• Bernhard Beckert, Steffen Schlager:
  A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities. 626-641
  
• Wolfgang Reif, Gerhard Schellhorn, Andreas Thums:
  Flaw Detection in Formal Specifications. 642-657
  
• Jürgen Avenhaus, Bernd Löchner:
  CCE: Testing Ground Joinability. 658-662
  
• Alessandro Armando, Luca Compagna, Silvio Ranise:
  System Description: RDL : Rewrite and Decision Procedure Laboratory. 663-669
  
• Joshua S. Hodas, Naoyuki Tamura:
  lolliCop - A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic. 670-684
  

Nonclassical Logics

• Dominique Pastre:
  MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction. 685-689
  
• Jörg Lücke:
  Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory. 690-695
  
• Dominique Larchey-Wendling, Dominique Méry, Didier Galmiche:
  STRIP: Structural Sharing for Efficient Proof-Search. 696-700
  
• Volker Haarslev, Ralf Möller:
  RACER System Description. 701-706
  

Last update Thu May 23 16:28:45 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page