Taming First-Order 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
|
|
|
Taming First-Order Logic
|
| Id. |
46242487 |
| Idioma |
inglés
|
| Titulo |
Taming First-Order Logic |
| Autor(es) |
Szabolcs Mikul As
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.7279
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
In this paper we define computationally well-behaved versions of classical first-order logic and prove that the validity problem is decidable 1 . Keywords : first-order logic, decidability, relativization, mosaic, polyadic and counting quantifiers. 1Taming In [5], we developed a strategy for taming logics. The idea of taming can be described as follows. Let us assume that we have a well-investigated logic with some undesirable metalogical properties. An example is the incompleteness and undecidability of the finite variable fragment of classical first-order logic, FOL, with at least three variables, cf. [4] 4.1.3 and 4.2.18 for the equivalent algebraic results. Taming a logic amounts to finding a version of the logic such that (i) this version has nicer properties than the original logic and (ii) its power is close to that of the original logic. Usually, one can achieve these two goals in two steps: (a) by weakening the logic (e.g., by widening the class of models) such that the weakened logic has desirable properties, and (b) by strengthening this weakened version (e.g., by (re-)introducing connectives that are not definable after weakening) without losing the nice properties. In [5], we stated that if we relativize the square version of pair arrow logic with arbitrary, or with reflexive and/or symmetric relations, then these relativized versions have nicer properties, e.g., they are complete and decidable. In pair arrow logic relativization amounts to the following. In the square version, the frames are Cartesian spaces: W = U U . In the relativized versions we require that W be an arbitrary, or a reflexive and/or symmetric relation. Further, we could strengthen these relativized versions by adding the di#erence operator to the language without losing completenes...
|
| Tipo |
application/pdf
|
| Palabras clave |
first-order 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/pdf
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] http://www.oup.co.uk/igpl/Volume_06/Issue_02/pdf/Mikulas.pdf
[References] 10.1.1.45.4756
[References] 10.1.1.46.386
|
| Fecha de contribución |
22-jul-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
