A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction
|
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
|
|
|
A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction
|
| Id. |
46388449 |
| Idioma |
inglés
|
| Titulo |
A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction |
| Autor(es) |
Jean Goubault-larrecq
Jean Goubault-larrecq
Projet Coq
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8976
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
: Proof systems like Coq feature inductive datatypes, where datatype constructors are free in the sense that two terms built from constructors only are semantically equal if and only if they are syntactically identical. Although free constructors are an essential ingredient of modern formalized mathematics, no automated first-order prover has been specialized with built-in rules for dealing with free constructors, until now. We propose a sequent system for a logic where terms can be built only from variables and free constructors. Thus the logic will be kept simple, as equality in the logic will be syntactical equality. We show how partial functions can be introduced into the logic, in the form of predicates obeying some functionality constraints. We prove that the resulting system is sound and complete with respect to a natural first-order semantics of datatypes, and enjoys cut elimination. We then develop a tableau calculus to find proofs in this sequent system. This involves solving...
|
| Tipo |
application/postscript
|
| Palabras clave |
logic
|
| Tipo de recurso |
Texto Narrativo
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| Formatos |
application/postscript
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-3653.ps.gz
|
| Fecha de contribución |
24-jul-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
