We consider a proof procedure aiming at refuting clause sets containing arithmetic constants
(or parameters), interpreted as natural numbers. The superposition calculus is enriched with …

In first-order logic, the formula-based instances of the Noetherian induction principle allow to
perform effectively simultaneous, mutual and lazy induction reasoning. Compared to the …

CLKID^ ω ω is a sequent-based cyclic inference system able to reason on first-order logic
with inductive definitions. The current approach for verifying the soundness of CLKID^ ω ω …

Les systèmes collaboratifs sont utilisés pour former un groupe de personnes réparti dans le
temps, l'espace et à travers des organisations [27]. Ces personnes collaborent ensemble le …

SPIKE, an induction-based theorem prover built to reason on conditional theories with
equality, is one of the few formal tools able to perform automatically mutual and lazy …

Rewriting induction (Reddy, 1990) is an automated proof method for inductive theorems of
term rewriting systems. Reasoning by the rewriting induction is based on the noetherian …

We give evidence of the direct integration and automated checking of implicit induction-
based proofs inside certified reasoning environments, as that provided by the Coq proof …

Theorem proving is crucial for the formal validation of properties about user specifications.
With the help of the Coq proof assistant, we show how to certify properties about conditional …

Largely adopted by proof assistants, the conventional induction methods based on explicit
induction schemas are non-reductive and local, at schema level. On the other hand, the …

We propose a new (Noetherian) induction schema to reason on equalities and show how to
integrate it into implicit induction-based inference systems. Non-orientable conjectures of the …