Informes técnicos de investigación DSIC-ELP
Permanent URI for this collection
Colección de documentos de trabajo, informes técnicos y otro material de investigación realizado por los investigadores del Departamento de Sistemas Informáticos y Computación (DSIC). Grupo ELP: Extensiones de la Programación Lógica (Extensions of Logic Programming) de la Universitat Politècnica de València en el desarrollo de sus investigaciones.
Browse
Recent Submissions
Now showing 1 - 5 of 15
- PublicationA Probabilistic Framework for Non-Cheating Machine Teaching(2022-05-03T05:59:23Z) Ferri Ramírez, César; Hernández Orallo, José; Telle, Jan Arne; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia ArtificialOver the past decades in the field of machine teaching, several restrictions have been introduced to avoid ‘cheating’, such as collusion-free or non-clashing teaching. However, these restrictions forbid several teaching situations that we intuitively consider natural and fair, especially those ‘changes of mind’ of the learner as more evidence is given, affecting the likelihood of concepts and ultimately their posteriors. Under a new generalised probabilistic teaching, not only do these non-cheating constraints look too narrow but we also show that the most relevant machine teaching models are particular cases of this framework: the consistency graph between concepts and elements simply becomes a joint probability distribution. We show a simple procedure that builds the witness joint distribution from the ground joint distribution. We prove a chain of relations, also with a theoretical lower bound, on the teaching dimension of the old and new models. Overall, this new setting is more general than the traditional machine teaching models, yet at the same time more intuitively capturing a less abrupt notion of non-cheating teaching.
- PublicationNarrowing-based Optimization of Rewrite Theories(Universitat Politècnica de València, 2020-06-08T06:04:05Z) Alpuente Frasnedo, María; Ballis, Demis; Escobar Román, Santiago; Sapiña Sanchis, Julia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; Agencia Estatal de Investigación; Generalitat ValencianaPartial evaluation has been never investigated in the context of rewrite theories that allow concurrent systems to be specified by means of rules, with an underlying equational theory being used to model system states as terms of an algebraic data type. In this paper, we develop a symbolic, narrowing-driven partial evaluation framework for rewrite theories that supports sorts, subsort overloading, rules, equations, and algebraic axioms. Our partial evaluation scheme allows a rewrite theory to be optimized by specializing the plugged equational theory with respect to the rewrite rules that define the system dynamics. This can be particularly useful for automatically optimizing rewrite theories that contain overly general equational theories which perform unnecessary computations involving matching modulo axioms, because some of the axioms may be blown away after the transformation. The specialization is done by using appropriate unfolding and abstraction algorithms that achieve significant specialization while ensuring the correctness and termination of the specialization. Our preliminary results demonstrate that our transformation can speed up a number of benchmarks that are difficult to optimize otherwise.
- PublicationAbstract Contract Synthesis and Verification in the Symbolic K Framework(Universitat Politècnica de València, 2018-04-12) Alpuente Frasnedo, María; Pardo Pont, Daniel; Villanueva García, Alicia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; European Regional Development Fund; Ministerio de Economía y Competitividad; Ministerio de Educación, Cultura y Deporte; Generalitat Valenciana[EN] In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the K semantic framework, we enrich the symbolic execution facilities recently provided by K with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KindSpec 2.1, which generates logical axioms that express pre- and postcondition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by K, some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our framework with little effort.
- PublicationStatic Correction of Maude Programs with Assertions(Universitat Politècnica de València, 2018-04-12) Alpuente Frasnedo, María; Ballis, D.; Sapiña Sanchis, Julia; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia Artificial; Generalitat ValencianaIn this paper, we present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification A of the program behavior that is given in the form of assertions together with an overly general program R whose execution might violate the assertions. Our technique translates R into a refined program R' in which every computation is a computation in R that satisfies the assertions of A. Our correction technique is first formalized for topmost rewrite theories, and then we generalize it to larger rewrite theories that support nested structured configurations. Our technique copes with infinite space states and does not require the knowledge of any failing run. We report experiments that assess the effectiveness of assertion-driven correction.
- PublicationI.G(Universitat Politècnica de València, 2018-04-12) Hernández Orallo, José; Departamento de Sistemas Informáticos y Computación; Escuela Técnica Superior de Ingeniería Informática; Instituto Universitario Valenciano de Investigación en Inteligencia ArtificialThis report summarises the key ideas for a simple concept of I.G. and its explanatory value for several areas.
- «
- 1 (current)
- 2
- 3
- »