Quantifier-free induction for lists

MaRDI QIDQ6436650zbMATH OpenFDO

Authors Stefan Hetzl, Jannik Vierling

Publication date 15 May 2023

Abstract: We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list $mathitnil$ and the operation $mathitcons$, that adds an element to the front of a list. First we show that, for $mgeq1$, quantifier-free $m$-step induction does not simulate quantifier-free $(m+1)$-step induction. Secondly, we show that for all $mgeq1$, quantifier-free $m$-step induction does not prove the right cancellation property of the concatenation operation on lists defined by left-recursion.

This page was built for publication: Quantifier-free induction for lists

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6436650)