TY - GEN
T1 - Interfacing HOL90 with a functional database query language
AU - Gunter, Elsa L.
AU - Libkin, Leonid
N1 - Publisher Copyright:
© 1995, Springer-Verlag. All rights reserved.
PY - 1995
Y1 - 1995
N2 - We describe a functional database language OR-SML for handling disjunctive information in database queries, its implementation in Standard ML [10], and its interface to HOL90. The core language has the power of the nested relational algebra, and it is augmented with or-sets which are used to deal with disjunctive information. Sets, or-sets and tuples can be freely combined to create objects, which gives the language a greater flexibility. We give an example of queries over the "database" of HOLg0 theories which require disjunctive information and show how to use the language to answer these queries. Since the system is running on top of Standard ML and all database objects are values in the latter, the system benefits from combining a sophisticated query language with the full power of a programming language. The language has been implemented as an HOL90-1oadable library of modules in Standard ML.
AB - We describe a functional database language OR-SML for handling disjunctive information in database queries, its implementation in Standard ML [10], and its interface to HOL90. The core language has the power of the nested relational algebra, and it is augmented with or-sets which are used to deal with disjunctive information. Sets, or-sets and tuples can be freely combined to create objects, which gives the language a greater flexibility. We give an example of queries over the "database" of HOLg0 theories which require disjunctive information and show how to use the language to answer these queries. Since the system is running on top of Standard ML and all database objects are values in the latter, the system benefits from combining a sophisticated query language with the full power of a programming language. The language has been implemented as an HOL90-1oadable library of modules in Standard ML.
UR - http://www.scopus.com/inward/record.url?scp=84957886156&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84957886156&partnerID=8YFLogxK
U2 - 10.1007/3-540-60275-5_64
DO - 10.1007/3-540-60275-5_64
M3 - Conference contribution
AN - SCOPUS:84957886156
SN - 3540602755
SN - 9783540602750
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 171
EP - 185
BT - Higher Order Logic Theorem Proving and Its Applications - 8th International Workshop, Proceedings
A2 - Schubert, E. Thomas
A2 - Windley, Phillip J.
A2 - Alves-Foss, James
PB - Springer
T2 - 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, 1995
Y2 - 11 September 1995 through 14 September 1995
ER -