A Framework for Defining Declarative Languages

  • Declarative languages are an important family of formalisms used for formal knowledge representation in computer science. Examples include logics, type theories, set theories, specification languages and ontology languages. Despite the vast variety of declarative languages, they share a common structure: A possibly infinite collection of theories, which are sets of declarations, and a set of well-formed expressions over each theory. This PhD thesis contributes to the design of declarative logical frameworks that balances the trade-off between abstract and concrete representations of declarative languages. In particular, we identify a new feature that can be added to a declarative framework as a language primitive: declaration patterns. The main idea behind this feature is to capture the common structure of the theories of declarative languages. More specifically, we reify declaration patterns as a language primitive for declarative logical frameworks and use them to characterize the legal declarations of non-logical symbols by specifying their syntactic shape. Then, we introduce a notion of pattern-based translation, which maps legal theories of one declarative language to legal theories of the other language. We introduce these novel notions in a calculus-based meta-framework for defining declarative languages and translations between them. Our meta-framework is independent of the underlying declarative logical framework and can be instantiated with specific logical frameworks like LF. In particular we develop a new declarative logical framework LFS (LF with sequences) that supports sequences and dependent function spaces that take sequence arguments, which we need for writing down the declaration patterns of most declarative languages. We apply and evaluate our pattern-based approach in an atlas of declarative languages, which includes various logics ranging from traditional first-order logic to more complex languages such as polymorphic higher order logic.

Download full text

Cite this publication

  • Export Bibtex
  • Export RIS

Citable URL (?):

Search for this publication

Search Google Scholar Search Catalog of German National Library Search OCLC WorldCat Search Catalog of GBV Common Library Network Search Catalog of Jacobs University Library Search Bielefeld Academic Search Engine
Meta data
Publishing Institution:IRC-Library, Information Resource Center der Jacobs University Bremen
Granting Institution:Jacobs Univ.
Author:Feryal Fulya Horozal
Referee:Michael Kohlhase, Dieter Hutter, Herbert Jäger, Till Mossakowski, Carsten Schürmann
Advisor:Michael Kohlhase
Persistent Identifier (URN):urn:nbn:de:gbv:579-opus-1004952
Document Type:PhD Thesis
Language:English
Date of Successful Oral Defense:2014/11/14
Year of Completion:2014
Date of First Publication:2014/12/08
PhD Degree:Computer Science
School:SES School of Engineering and Science
Other Countries Involved:Denmark
Library of Congress Classification:Q Science / Q Science (General) / Q300-390 Cybernetics / Q325-342 Self-organizing systems. Conscious automata / Q350-390 Information theory / Q387 Knowledge representation / Q387.3 Description logics
Call No:Thesis 2014/31

$Rev: 13581 $