In this paper we present finitary proof systems for the deduction
of sentences from algebraic specifications inductively defined by
specification expresssions in first-order and higher-order logic.
Mainly, we redesign the proof systems for the reachability and
The main application of the result is to give an adequate representation
of this kind of proof systems in a type-theoretic logical framework.
Mylonakis, N. "Finitary non-compositional proof systems for ASL in first-order". 2003.