Person: Nieva Soto, Susana
Universidad Complutense de Madrid
Faculty / Institute
Sistemas Informáticos y Computación
Lenguajes y Sistemas Informáticos
Now showing 1 - 10 of 11
PublicationHigher-order logic programming languages with constraints: A semantics(Springer Verlag Berlín, 2007) Nieva Soto, Susana; Lipton, James; Ronchi della Rocca, SimonaA Kripke Semantics is defined for a higher-order logic programming language with constraints, based on Church's Theory of Types and a generic constraint formalism. Our syntactic formal system, hoHH(C) (higher-order hereditary Harrop formulas with constraints), which extends lambda Prolog's logic, is shown sound and complete. A Kripke semantics for equational reasoning in the simply typed lambda-calculus (Kripke Lambda Models) was introduced by Mitchell and Moggi in 1990. Our model theory extends this semantics to include full impredicative higher-order intuitionistic logic, as well as the executable hoHH fragment with typed lambda-abstraction, implication and universal quantification in goals and constraints. This provides a Kripke semantics for the full higher-order hereditarily Harrop logic of lambda Prolog as a special case (with the constraint system chosen to be,13,beta,eta-conversion). PublicationMIZ-PR: A theorem prover for polymorphic and recursive functions(Springer Verlag, 1992) Leach Albert, Javier; Nieva Soto, Susana PublicationMIZ-PR: A Theorem Prover for Polymorphic and Recursive Functions(Springer Verlag, 1992) Leach Albert, Javier; Nieva Soto, Susana; Voronkov , Andrei PublicationR-SQL: An SQL Database System with Extended Recursion(2013) Aranda López, Gabriel; Nieva Soto, Susana; Sáenz Pérez, Fernando; Sánchez Hernández, JaimeThe relational database language SQL:1999 standard supports recursion, but thisapproach is limited to the linear case. Moreover, mutual recursion is not supported,and negation cannot be combined with recursion. We designed the language R-SQLto overcome these limitations in [ANSS13], improving termination properties in re-cursive definitions. In addition we developed a proof of concept implementation ofan R-SQL system. In this paper we describe in detail an improved system enhanc-ing performance. It can be integrated into existing RDBMS’s, extending them withthe aforementioned benefits of R-SQL. The system processes an R-SQL databasedefinition obtaining its extension in tables of an RDBMS (such as PostgreSQL andDB2). It is implemented in SWI-Prolog and it produces a Python script that, uponexecution, computes the result of the R-SQL relations. We provide some perfor-mance results showing the efficiency gains w.r.t. the previous version. We alsoinclude a comparative analysis including some representative relational a deductive systems. PublicationA higher-order logic programming language with constraints(Springer Verlag, 2001) Nieva Soto, Susana; Leach Albert, JavierWe present a framework for the combination of Constraint Logic Programming (tiCLP) and higher-order Hereditary Harrop Formulas (tihoHH). Our aim is to improve the expressiveness of traditional Logic Programming with the benefits of both fields: tiCLP and tihoHH. The result is denoted higher-order Hereditary Harrop Formulas with Constraints (hoHH(C)). The syntax of hoHH is introduced using lambda-terms and is enriched with a basic constraint system. Then an intuitionistic sequent calculus is defined for this combined logic, that preserves the property of an abstract logic programming language. In addition, a sound and complete procedure for goal solving is presented as a transformation system that explains the operational semantics. PublicationUna lógica computacional con polimorfismo y recursión y un sistema de deducción automática basado en ella(Universidad Complutense de Madrid, 2015) Nieva Soto, Susana; Leach Albert, JavierEn la primera parte de la memoria se presenta una logica computacional, que es una logica de predicados con igualdad extendida con polimorfismo y recursion, junto con un sistema de deduccion natural, para esta logica se da una definicion precisa de su semantica y se demuestran buenas propiedades. Se comprueba que es adecuada para razonar acerca de funciones parciales, minimo punto fijo de funcionales y semantica denotacional, y para hacer demostraciones matematicas. Se presenta tambien una extension de los tableaux de Shullyan de primer orden que supone el uso de arboles w-ramificados e instancias monomorfica de las formulas de partida. El algoritmo de los tableaux se utiliza como guia en la construccion de calculos completos. Utilizndo esta propiedad se construye un sistema de reglas de deduccion natural y se prueba que como todo calculo ... PublicationImplementing a Fixpoint Semantics for a Constraint Deductive Database based on Hereditary Harrop Formulas(Assoc Computing Machinery, 2009) Aranda López, Gabriel; Nieva Soto, Susana; Sáenz Pérez, Fernando; Sánchez Hernández, JaimeThis work is aimed to show a concrete implementation of a deductive database system based on the scheme HH-(C) (Hereditary Harrop Formulas with Negation and Constraints) following a fixpoint semantics proposed in a previous work. We have developed a Prolog implementation for this scheme that is constraint system independent. therefore allowing to use it as a base for any instance of the formal scheme. We have developed several specific constraint systems: Real numbers, integers, Boolean and user-defined enumerated types. We have added types to the database so that relations become typed (as tables in relational databases) and each constraint is mapped to its corresponding constraint system. The predicates that compute the fixpoint giving the meaning to a database are described. In particular, we show the implementation of a forcing relation (for derivation steps) and highlight how the inherent difficulties have been overcome in a system allowing hypothetical queries, which make the database dynamically grow. PublicationFormalizing a constraint deductive database language based on hereditary harrop formulas with negation(Springer-Verlag Berlín, 2008) Nieva Soto, Susana; Sánchez-Hernández, Jaime; Sáenz-Pérez, Fernando; Garrigue, Jacques; Hermenegildo, ManuelIn this paper, we present an extension of the scheme HH(C) (Hereditary Harrop formulas with Constraints) with a suitable formulation of negation in order to obtain a constraint deductive database query language. In addition to constraints, our proposal includes logical connectives (implication and quantifiers) for defining databases and queries, which altogether are unavailable in current database query languages. We define a proof theoretic semantic framework based on a sequent calculus, that allows to represent the meaning of a database query by means of a derived constraint answer in the sense of CLP. We also introduce an appropriate notion of stratification, which provides a starting point for suitable operational semantics dealing with recursion and negation. We formalize a fixed point semantics for stratifiable databases, whose fixpoint operator is applied stratum by stratum. This semantics is proved to be sound and complete with respect to derivability in the sequent calculus, and it provides the required support for actual implementations, as the prototype we have developed already and introduce in this paper. PublicationExtending Liquid Types to Arrays(ACM, 2020-01-21) Montenegro Montes, Manuel; Nieva Soto, Susana; Peña Marí, Ricardo; Segura Díaz, Clara MaríaA liquid type is an ordinary Hindley-Milner type annotated with a logical predicate that states the properties satisfied by the elements of that type. Liquid types are a powerful tool for program verification, since programmers can use them to specify pre- and postconditions of their programs, while the predicates of intermediate variables and auxiliary functions are inferred automatically. Type inference is feasible in this context, since the logical predicates within liquid types are constrained to a quantifier-free logic in order to maintain decidability. In this paper we extend liquid types by allowing them to contain quantified properties on arrays, so that they can be used to infer invariants on array-related programs (for example, implementations of sorting algorithms). Although quantified logic is, in general, undecidable, we restrict properties on arrays to a decidable subset introduced by Bradley et al. We describe in detail the extended type system, the verification condition generator, and the iterative weakening algorithm for inferring invariants. After proving the correctness and completeness of these two algorithms, we apply them to find invariants on a set of algorithms involving array manipulations. PublicationConstraint Logic Programming with Hereditary Harrop formulas(Cambridge Univ Press, 2001-07) Leach Albert, Javier; Nieva Soto, Susana; Rodríguez-Artalejo, MarioConstraint Logic Programming (CLP) and Hereditary Harrop formulas (HH) are two well known ways to enhance the expressivity of Horn clauses. In this paper, we present a novel combination of these two approaches. We show how to enrich the syntax and proof theory of HH with the help of a given constraint system, in such a way that the key property of HH as a logic programming language (namely, the existence of uniform proofs) is preserved. We also present a procedure for goal solving, showing its soundness and completeness for computing answer constraints. As a consequence of this result, we obtain a new strong completeness theorem for CLP that avoids the need to build disjunctions of computed answers, as well as a more abstract formulation of a known completeness theorem for HH.