- Online First™
The HOL Light Theory of Euclidean Space
John Harrison
Online First™, 3 May 2012
- Online First™Open Access
Uncurrying for Termination and Complexity
Nao Hirokawa, Aart Middeldorp and Harald Zankl
Online First™, 25 April 2012
- Online First™Open Access
Multi-Completion with Termination Tools
Sarah Winkler, Haruhiko Sato, Aart Middeldorp and Masahito Kurihara
Online First™, 14 April 2012
- Online First™
6 Years of SMT-COMP
Clark Barrett, Morgan Deters, Leonardo de Moura, Albert Oliveras and Aaron Stump
Online First™, 31 March 2012
- Online First™
Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions
James P. Bridge and Lawrence Charles Paulson
Online First™, 5 March 2012
- Online First™
Paramodulation with Non-Monotonic Orderings and Simplification
Miquel Bofill and Albert Rubio
Online First™, 15 December 2011
- Online First™
ExpTime Tableaux for ALC\boldsymbol{\mathcal{ALC}} Using Sound Global Caching
Rajeev Goré and Linh Anh Nguyen
Online First™, 9 December 2011
- Online First™
Invariant-Free Clausal Temporal Resolution
Jose Gaintzarain, Montserrat Hermo, Paqui Lucio, Marisa Navarro and Fernando Orejas
Online First™, 2 December 2011
- Online First™
Simulating Circuit-Level Simplifications on CNF
Matti Järvisalo, Armin Biere and Marijn J. H. Heule
Online First™, 3 November 2011
- Online First™
PSPACE Tableau Algorithms for Acyclic Modalized ALC\boldsymbol{\mathcal{ALC}}
Jia Tao, Giora Slutzki and Vasant Honavar
Online First™, 9 July 2011