An Extension of a First-Order Language and Its Applications (Many-Sorted Logic, Distributed Database Design, Resolution, Automatic Theorem Proving, Horizontal Partitioning).

Abstract

In the currently known many-sorted logic, a variable ranging over a sort that does not exist in the sort structure cannot be introduced. To avoid this problem extended calculi are proposed that are obtained by embedding a new kind of syntactic object called aggregate variables in a one-sorted language and in a many-sorted language. The resulting languages are called, respectively, a one-sorted language with aggregate variables, denoted by L(,(SIGMA))('1) and a many-sorted language with aggregate variables, denoted by L(,(SIGMA)). Theoretic foundation for the extended predicate calculi is provided and their practical usage in real applications is demonstrated: L(,(SIGMA)), in the distributed database design area and L(,(SIGMA))('1), in the automatic theorem proving area. As an application in the distributed design area, L(,(SIGMA)) is used for the representation of the user queries and the knowledge about data. A knowledge-based approach is proposed with which the user reference clusters (URC's) to a database are estimated. The URC's can then be used in partitioning a relational database horizontally during distributed database design. Using the knowledge about the data, the user queries are converted to equivalent queries by a proposed inference procedure. The URC's that were estimated from these revised queries are more precise than those that can be estimated from the original user queries. The types of knowledge to be used are discussed. An example illustrates the way inference is carried out, and the correctness of the inference is also discussed. As an application L(,(SIGMA))('1) in the automatic theorem proving area, a type of problem is first identified which may occur when a resolution scheme is applied to many-sorted theory. It is shown that any many-sorted theory can be converted into an equivalent theory in L(,(SIGMA))('1). Aggregate variables allow the introduction of range-restricted variables dynamically in the structure which is exp and ed by definitions. This allows the introduction of a new resolution scheme named Unification over the Weakest Range (or UWR-resolution). The completeness of UWR-resolution is shown and the efficiency of UWR-resolution is discussed.