|
Title:
|
Finitary non-compositional proof systems for ASL in first-order
|
|
Author:
|
Mylonakis Pascual, Nicolás
|
|
Other authors:
|
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació |
|
Abstract:
|
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. |
|
Subject(s):
|
-Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica
-Proof systems
-Algebraic specifications
-Reachability
-Behavioural operators
-First-order logic
-Higher-order logic |
|
Rights:
|
|
|
Document type:
|
Article - Published version
Report |
|
Share:
|
|
