Yet another decision procedure for equality 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
|
|
|
Yet another decision procedure for equality logic
|
| Id. |
45729051 |
| Idioma |
inglés
|
| Titulo |
Yet another decision procedure for equality logic |
| Autor(es) |
Orly Meir
Ofer Strichman
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.4673
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
Abstract. We introduce a new decision procedure for Equality Logic. The procedure improves on Bryant and Velev’s sparse method [4] from CAV’00, in which each equality predicate is encoded with a Boolean variable, and then a set of transitivity constraints are added to compensate for the loss of transitivity of equality. We suggest the Reduced Transitivity Constraints (rtc) algorithm, that unlike the sparse method, considers the polarity of each equality predicate, i.e. whether it is an equality or disequality when the given equality formula ϕ E is in Negation Normal Form (NNF). Given this information, we build the Equality Graph corresponding to ϕ E with two types of edges, one for each polarity. We then define the notion of Contradictory Cycles to be cycles in that graph that the variables corresponding to their edges cannot be simultaneously satisfied due to transitivity of equality. We prove that it is sufficient to add transitivity constraints that only constrain Contradictory Cycles, which results in only a small subset of the constraints added by the sparse method. The formulas we generate are smaller and define a larger solution set, hence are expected to be easier to solve, as indeed our experiments show. Our new decision procedure is now implemented in the uclid verification system.
|
| Tipo |
application/pdf
|
| Palabras clave |
Equality 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://iew3.technion.ac.il/~ofers/publications/cav05_full.pdf
[References] 10.1.1.24.7475
[References] 10.1.1.17.8352
[References] 10.1.1.11.2290
[References] 10.1.1.25.9103
[References] 10.1.1.52.1007
[References] 10.1.1.36.2061
[References] 10.1.1.5.501
[References] 10.1.1.68.2512
[References] 10.1.1.2.6310
[References] 10.1.1.37.2403
[References] 10.1.1.97.5479
[References] 10.1.1.132.3202
[References] 10.1.1.81.3893
[References] 10.1.1.95.4461
[References] 10.1.1.137.5568
[References] 10.1.1.144.9343
|
| Fecha de contribución |
27-sep-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
