Skip to content
Norbert Preining edited this page Oct 6, 2017 · 2 revisions

CITP

Constructor Based Induction Theorem Prover

The sub-system provides a certain level of automatization for theorem proving.

Please see the accompanying manual for CITP for details.

Related: :attr, :reset, :embed, :use, :ord, :imp, :def, :ctf-, :ctf, :csp-, :csp, :red, :select, :backward, :rule, :equation, :cp, :init, :roll, :auto, :ind, :apply, :goal

Clone this wiki locally