Higher-Order Equational Logic
|
Descargar SCORM
Este recurso ha sido solicitado 1 veces (0 veces en los últimos 31 días).
Para poder solicitar este recurso debe identificarse como usuario de la biblioteca
|
| |
Ver
Detalles del recurso
|
|
|
Higher-Order Equational Logic
|
| Id. |
41795309 |
| Idioma |
inglés
|
| Titulo |
Higher-Order Equational Logic |
| Autor(es) |
Christian Prehofer,Tu Munchen,Contributions From Tobias Nipkow,C. Prehofer,Higher-order Equational Logic
|
| Localización |
http://citeseer.ist.psu.edu/359949.html
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
Syntax"
[Pfenning&Elliot 88]
Applications: Programming languages, mathematics, formal
systems
ffl Higher-order theorem proving
ffl Declarative Programming
C. Prehofer, 6/97 Higher-Order Equational Logic 4
Declarative Programming Paradigms
?
XXXXXXXXX Xz
XXXXXXXXX Xz
9
9
?
Logic Programming Functional Programming
Narrowing
Higher-Order LP Higher-Order FP
Higher-Order Narrowing
C. Prehofer, 6/97 Higher-Order Equational Logic 5
Notation and Basic Definitions
Variable Conventions
ffl F; G; H;X;Y free variables
ffl a; b; c; f; g (function) constants
ffl x; y; z bound variables
ffl ff; fi type variables
ffl u,v,w constants or bound variables
-terms: t = F j x j c j x:t j (t 1 t 2 )
Note:
x n :s = x 1 : : : x n :s
a(s n ) = ((Delta Delta Delta (a s 1 ) Delta Delta Delta) s n )
C. Prehofer, 6/97 Higher-Order Equational Logic 6
Conversions in -Calculus
ff-conversion: x:t = ff y:(t[x 7! y])
fi-conversion: (x:s)t = fi s[x 7! t])
j-conversion: if x = 2 FV(t), t...
|
| Tipo |
ps
|
| Palabras clave |
Christian Prehofer,Tu Munchen,Contributions From Tobias Nipkow,C. Prehofer,Higher-order Equational Logic Higher-Order Equational Logic
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
unrestricted |
| Formatos |
ps
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] http://www4.informatik.tu-muenchen.de/~prehofer/cade-tut.ps.gz
[References] oai:CiteSeerPSU:306753
[References] oai:CiteSeerPSU:27540
[References] oai:CiteSeerPSU:25394
[References] oai:CiteSeerPSU:339983
[References] oai:CiteSeerPSU:337057
[References] oai:CiteSeerPSU:642441
[References] oai:CiteSeerPSU:500973
[References] oai:CiteSeerPSU:88938
[References] oai:CiteSeerPSU:309043
[References] oai:CiteSeerPSU:8668
[References] oai:CiteSeerPSU:67090
[References] oai:CiteSeerPSU:172610
[References] oai:CiteSeerPSU:128823
[References] oai:CiteSeerPSU:163647
[References] oai:CiteSeerPSU:678243
[References] oai:CiteSeerPSU:132961
[References] oai:CiteSeerPSU:306170
[References] oai:CiteSeerPSU:150352
[References] oai:CiteSeerPSU:4445
|
| Fecha de contribución |
31-mar-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
