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