haRVey: combining reasonersReportar como inadecuado




haRVey: combining reasoners - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 UFRN - Universidade Federal do Rio Grande do Norte Natal 2 MOSEL - Proof-oriented development of computer-based systems INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

Abstract : We present the architecture of the oncoming version of the SMT Satisfiability Modulo Theories solver haRVey. haRVey checks the satisfiability of a formula written in a first-order language with interpreted symbols from various theories. Its new architecture is original, first in the sense that it is a combination of reasoners, rather than the traditional combination of decision procedures. Second, one of these reasoners is a full-featured first-order saturation-based prover. Finally, some of those reasoners in the combination may only be sporadically activated not using computer time when inactive. We believe those new features will contribute to the efficiency and expressivity of the new version of the tool.





Autor: David Déharbe - Pascal Fontaine -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados