Reasoning with TriggersReportar como inadecuado

Reasoning with Triggers - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

* Corresponding author 1 PROVAL - Proof of Programs UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR 2 LRI - Laboratoire de Recherche en Informatique

Abstract : SMT solvers can decide the satisfiability of ground formulas modulo a combination of built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures. In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate on two examples, how such proofs can be achieved in our formalism.

Keywords : Quantifiers Triggers SMT Solvers Theories

Autor: Claire Dross - Sylvain Conchon - Andrei Paskevich -



Documentos relacionados