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

Consultar RECERCAT

Per accedir als documents amb el text complet, si us plau, seguiu el següent enllaç: http://hdl.handle.net/2117/95933

dc.contributor	Universitat Politècnica de Catalunya. Departament de Ciències de la Computació
dc.contributor.author	Mylonakis Pascual, Nicolás
dc.date	2003-03-02
dc.identifier.citation	Mylonakis, N. "Finitary non-compositional proof systems for ASL in first-order". 2003.
dc.identifier.uri	http://hdl.handle.net/2117/95933
dc.language.iso	eng
dc.relation	R00-21
dc.rights	info:eu-repo/semantics/openAccess
dc.subject	Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica
dc.subject	Proof systems
dc.subject	Algebraic specifications
dc.subject	Reachability
dc.subject	Behavioural operators
dc.subject	First-order logic
dc.subject	Higher-order logic
dc.title	Finitary non-compositional proof systems for ASL in first-order
dc.type	info:eu-repo/semantics/publishedVersion
dc.type	info:eu-repo/semantics/report
dc.description.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.

Mylonakis Pascual, Nicolás; Orejas Valdés, Fernando; Fiadeiro, José

Mylonakis Pascual, Nicolás

Mylonakis Pascual, Nicolás; Orejas Valdés, Fernando

Mylonakis Pascual, Nicolás; Orejas Valdés, Fernando

Mylonakis Pascual, Nicolás; Orejas Valdés, Fernando

Coordinació

Patrocini