We propose a new cyclic proof system for automated, equational reasoning about the
behaviour of pure functional programs. The key to the system is the way in which cyclic …

Cyclic induction is a powerful reasoning technique that consists in blocking the proof
development of certain subgoals already encountered during the proof process. In the …

The constraints of pure functional programs are often applauded for the resulting safety and
correctness guarantees. It is also claimed that these programs are easier to reason about …

Abstract The international Erasmus+ European Project:“ARC–Automated Reasoning in the
Class”, running from 2019 to 2022 is a partnership of universities from Austria, France …

Résumé La récurrence nœthérienne est un des principes les plus généraux de
raisonnement formel. Dans le cadre du raisonnement de premier ordre, nous présentons …

Noetherian induction is one of the most general induction principles used in formal
reasoning. In the frame of the first-order reasoning, we propose a classification of its …

Cyclic induction is a more recent proof technique that can be applied for proof derivations
involving repetitive steps. Since repetition may be an infinite process, cyclic pre-proofs help …