Journal of Automated Reasoning (JAR), Volume 30

Volume 30, Number 1, January 2003

• Cesare Tinelli: Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing. 1-31
• Antonella Santone, Gigliola Vaglini: Modifying LOTOS Specifications by Means of Automatable Formula-Based Integrations. 33-58
• Fairouz Kamareddine, Qiao Haiyan: Formalizing Strong Normalization Proofs of Explicit Substitution Calculi in ALF. 59-98
• Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio: Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. 99-120

Volume 30, Number 2, February 2003

• Andrei Voronkov: Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. 121-151
• Michaël Rusinowitch, Sorin Stratulat, Francis Klay: Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm. 53-177
• Larry Wos: The Strategy of Cramming. 179-204
• Krishnendu Chatterjee, Pallab Dasgupta, P. P. Chakrabarti: A Branching Time Temporal Framework for Quantitative Reasoning. 205-232

Volume 30, Numbers 3-4, 2003

• Tobias Nipkow:
  Java Bytecode Verification. 233-233
  
• Xavier Leroy:
  Java Bytecode Verification: Algorithms and Formalizations. 235-269
  
• Stephen N. Freund, John C. Mitchell:
  A Type System for the Java Bytecode Language and Verifier. 271-321
  
• Robert F. Stärk, Joachim Schmid:
  Completeness of a Bytecode Verifier and a Certifying Java-to-JVM Compiler. 323-361
  
• Gerwin Klein, Martin Wildmoser:
  Verified Bytecode Subroutines. 363-398
  
• David A. Basin, Stefan Friedrich, Marek Gawkowski:
  Bytecode Verification by Model Checking. 399-444