Abstract is missing.
- The Legacy of a Great ResearcherLarry Wos. 1-14 [doi]
- The Strategy Challenge in SMT SolvingLeonardo Mendonça de Moura, Grant Olney Passmore. 15-44 [doi]
- Simple and Efficient Clause Subsumption with Feature Vector IndexingStephan Schulz. 45-67 [doi]
- Superposition for Bounded DomainsThomas Hillenbrand, Christoph Weidenbach. 68-100 [doi]
- MACE4 and SEM: A Comparison of Finite Model GeneratorsHantao Zhang, Jian Zhang 0001. 101-130 [doi]
- Group Embedding of the Projective Plane PG(2, 3)Eric Ens, Ranganathan Padmanabhan. 131-138 [doi]
- A Geometric Procedure with Prover9Ranganathan Padmanabhan, Robert Veroff. 139-150 [doi]
- Loops with Abelian Inner Mapping Groups: An Application of Automated DeductionMichael K. Kinyon, Robert Veroff, Petr Vojtechovský. 151-164 [doi]
- (Dual) Hoops Have Unique HalvingRob Arthan, Paulo Oliva. 165-180 [doi]
- Gibbard's Collapse Theorem for the Indicative Conditional: An Axiomatic ApproachBranden Fitelson. 181-188 [doi]
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus InvariantsDeepak Kapur, Zhihai Zhang, Matthias Horbach, Hengjun Zhao, Qi Lu, ThanhVu Nguyen. 189-228 [doi]
- Toward a Procedure for Data Mining ProofsZachary Ernst, Seth Kurtenbach. 229-239 [doi]
- Theorem Proving in Large Formal Mathematics as an Emerging AI FieldJosef Urban, Jirí Vyskocil. 240-257 [doi]