Journal of Automated Reasoning (JAR), Volume 43

Volume 43, Number 1, June 2009

• Jasmin Christian Blanchette:
  Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm. 1-18
  
• Jean-François Dufourd:
  An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps. 19-51
  
• Raul Monroy, Alan Bundy, Ian Green:
  On Process Equivalence = Equation Solving in CCS. 53-80
  
• Filip Maric:
  Formalization and Implementation of Modern SAT Solvers. 81-119
  

Volume 43, Number 2, August 2009

• K. Subramani:
  Optimal Length Resolution Refutations of Difference Constraint Systems. 121-137
  
• Ruben A. Gamboa:
  A Formalization of Powerlist Algebra in ACL2. 139-172
  
• Harald Zankl, Nao Hirokawa, Aart Middeldorp:
  KBO Orientability. 173-201
  
• Giorgio Dalzotto, Tomás Recio:
  On Protocols for the Automated Discovery of Theorems in Elementary Geometry. 203-236