Abstract is missing.
- Efficient Instantiation Techniques in SMT (Work In Progress)Haniel Barbosa. 1-10 [doi]
- Alternative Treatments of Common Binary Relations in First-order Automated ReasoningKoen Claessen, Ann Lillieström. 11-23 [doi]
- No Choice: Reconstruction of First-order ATP Proofs without Skolem FunctionsMichael Färber, Cezary Kaliszyk. 24-31 [doi]
- Deduction as a ServiceMohamed Hassona, Stephan Schulz. 32-40 [doi]
- TH1: The TPTP Typed Higher-Order Form with Rank-1 PolymorphismCezary Kaliszyk, Geoff Sutcliffe, Florian Rabe. 41-55 [doi]
- Prover-independent Axiom Selection for Automated Theorem Proving in OntohubEugen Kuksa, Till Mossakowski. 56-68 [doi]
- On Checking Kripke Models for Modal Logic KJean-Marie Lagniez, Daniel Le Berre, Tiago De Lima, Valentin Montmirail. 69-81 [doi]
- Towards a Substitution Tree Based Index for Higher-order Resolution Theorem ProversTomer Libal, Alexander Steen. 82-94 [doi]
- Ordered Resolution with Straight Dismatching ConstraintsAndreas Teucke, Christoph Weidenbach. 95-109 [doi]
- A Saturation-based Algebraic Reasoner for ELQJelena Vlasenko, Maryam Daryalal, Volker Haarslev, Brigitte Jaumard. 110-124 [doi]
- The PIE Environment for First-Order-Based Proving, Interpolating and EliminatingChristoph Wernhard. 125-138 [doi]