Finitary non-compositional proof systems for ASL in first-order

Mylonakis Pascual, Nicolás

View/Open

R00-21.pdf (273,7Kb)

View UPCommons Usage Statistics

LA Referencia / Recolecta stats

Cita com:

Show full item record

Mylonakis Pascual, Nicolás

Document typeResearch report

Defense date2003-03-02

Rights accessOpen Access

All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder

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.

CitationMylonakis, N. "Finitary non-compositional proof systems for ASL in first-order". 2003.

Is part ofR00-21

URIhttp://hdl.handle.net/2117/95933

Collections

Departament de Ciències de la Computació - Reports de recerca [1.108]

View UPCommons Usage Statistics

Show full item record

Files	Description	Size	Format	View
R00-21.pdf		273,7Kb	PDF	View/Open

UPCommons. Global access to UPC knowledge

Finitary non-compositional proof systems for ASL in first-order

View/Open

Browse