Article
Synthesis of positive logic programs for checking a class of definitions with infinite quantification
Author/s | Galán Morillo, Francisco José
Cañete Valdeón, José Miguel |
Department | Universidad de Sevilla. Departamento de Lenguajes y Sistemas Informáticos |
Publication Date | 2016 |
Deposit Date | 2020-06-18 |
Published in |
|
Abstract | We describe a method based on unfold/fold transformations that synthesizes positive logicprograms P(r)with the purpose of checking mechanically definitions of the form D(r) =∀X(r(X) ⇔QYR(X, Y))where ris the relation defined ... We describe a method based on unfold/fold transformations that synthesizes positive logicprograms P(r)with the purpose of checking mechanically definitions of the form D(r) =∀X(r(X) ⇔QYR(X, Y))where ris the relation defined by the formula QYR(X, Y), Xis a set of variables to be instantiated at runtime by ground terms, QYis a set of quantifiedvariables on infinite domains (Qis the quantifier) and R(X, Y)a quantifier-free formulain the language of a first-order logic theory. This work constitutes a first step towards theconstruction of a new type of assertion checkers with the ability of handling restrictedforms of infinite quantification. |
Citation | Galán Morillo, F.J. y Cañete Valdeón, J.M. (2016). Synthesis of positive logic programs for checking a class of definitions with infinite quantification. Information and Computation, 249 (August 2016), 205-236. |
Files | Size | Format | View | Description |
---|---|---|---|---|
Synthesis of positive logic ... | 1.043Mb | [PDF] | View/ | |