INKA: The next generation

DOI10.1007/3-540-61511-3_92zbMath1412.68236OpenAlexW1490584023MaRDI QIDQ4647524

Dieter Hutter, Claus Sengler

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_92

zbMATH Keywords

automated deductioninductive proofsyntactical difference

Mathematics Subject Classification ID

Related Items (5)

Proving theorems by reuse ⋮ Termination of algorithms over non-freely generated data types ⋮ MBase: Representing knowledge and context for the integration of mathematical software systems ⋮ Plagiator — A learning prover ⋮ On terminating lemma speculations.

Uses Software

• InKa

Cites Work

• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• On proving the termination of algorithms by machine
• Coloring terms to control equational reasoning
• Termination of algorithms over non-freely generated data types

This page was built for publication: INKA: The next generation