Abstract is missing.
- Targeting Completeness: Using Closed Forms for Size Bounds of Integer ProgramsNils Lommen, Jürgen Giesl. 3-22 [doi]
- Recurrence-Driven Summations in Automated DeductionVisa Nummelin, Jasmin Blanchette, Sander R. Dahmen. 23-40 [doi]
- Formal Verification of Bit-Vector Invertibility Conditions in CoqBurak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett. 41-59 [doi]
- Weighted Path Orders Are Semantic Path OrdersTeppei Saito, Nao Hirokawa. 63-80 [doi]
- KBO Constraint Solving RevisitedYasmine Briefs, Hendrik Leidinger, Christoph Weidenbach. 81-98 [doi]
- A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting SystemsRyota Haga, Yuki Kagaya, Takahito Aoto 0001. 99-116 [doi]
- Logic of Communication Interpretation: How to Not Get Lost in TranslationGiorgio Cignarale, Roman Kuznets, Hugo Rincon Galeana, Ulrich Schmid 0001. 119-136 [doi]
- Symbolic Model Construction for Saturated Constrained Horn ClausesMartin Bromberger, Lorenz Leutgeb, Christoph Weidenbach. 137-155 [doi]
- Combining Finite Combination Properties: Finite Models and Busy BeaversGuilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett. 159-175 [doi]
- Formal Reasoning Using Distributed AssertionsFarah Al Wardani, Kaustuv Chaudhuri, Dale Miller 0001. 176-194 [doi]
- An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCLSibylle Möhle. 195-213 [doi]
- Hammering Floating-Point ArithmeticOlle Torstensson, Tjark Weber. 217-235 [doi]
- Learning Proof Transformations and Its Applications in Interactive Theorem ProvingLiao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban. 236-254 [doi]
- Translating SUMO-K to Higher-Order Set TheoryChad E. Brown, Adam Pease, Josef Urban. 255-274 [doi]