Finitary non-compositional proof systems for ASL in first-order
Nicolás Mylonakis Pascual · 2003
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 behavioural operators. The main application of the result is to give an adequate representation of this kind of proof systems in a type-theoretic logical framework.