Information and Computation, Volume 199

Volume 199, Numbers 1-2, 25 May 2005-15 June 2005

• Franz Baader:
  19th International Conference on Automated Deduction (CADE-19). 1-2
  
• Harald Ganzinger, Jürgen Stuber:
  Superposition with equivalence reasoning and delayed clause normal form transformation. 3-23
  
• Hans de Nivelle:
  Translation of resolution proofs into short first-order proofs without choice axioms. 24-54
  
• Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt:
  Mechanising first-order temporal resolution. 55-86
  
• Sava Krstic, Sylvain Conchon:
  Canonization for disjoint unions of theories. 87-106
  
• Sumit Gulwani, George C. Necula:
  A randomized satisfiability procedure for arithmetic and uninterpreted function symbols. 107-131
  
• Carsten Lutz, Ulrike Sattler, Lidia Tendera:
  The complexity of finite model reasoning in description logics. 132-171
  
• Nao Hirokawa, Aart Middeldorp:
  Automating the dependency pair method. 172-199
  
• Farhad Mehta, Tobias Nipkow:
  Proving pointer programs in higher-order logic. 200-227
  
• Alexandre Riazanov, Andrei Voronkov:
  Efficient instance retrieval with standard and relational path indexing. 228-252