Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
426980 | Information and Computation | 2016 | 32 Pages |
Abstract
We describe a method based on unfold/fold transformations that synthesizes positive logic programs P(r)P(r) with the purpose of checking mechanically definitions of the form D(r)=∀X(r(X)⇔QYR(X,Y))D(r)=∀X(r(X)⇔QYR(X,Y)) where r is the relation defined by the formula QYR(X,Y)QYR(X,Y), X is a set of variables to be instantiated at runtime by ground terms, QY is a set of quantified variables on infinite domains (Q is the quantifier) and R(X,Y)R(X,Y) a quantifier-free formula in the language of a first-order logic theory. This work constitutes a first step towards the construction of a new type of assertion checkers with the ability of handling restricted forms of infinite quantification.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Francisco J. Galán, José M. Cañete-Valdeón,