Termination Competition (termCOMP 2015)

DOI10.1007/978-3-319-21401-6_6zbMath1465.68282OpenAlexW1419314641MaRDI QIDQ3454084

Albert Rubio, Johannes Waldmann, Jürgen Giesl, René Thiemann, Frédéric Mesnard

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2117/85179

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

Automatic synthesis of logical models for order-sorted first-order theories ⋮ Termination of Cycle Rewriting by Transformation and Matrix Interpretation ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ Constant runtime complexity of term rewriting is semi-decidable ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ From Outermost to Context-Sensitive Rewriting

This page was built for publication: Termination Competition (termCOMP 2015)