Compiling Logics

Mihai Codescu, Fulya Horozal, Aivaras Jakubauskas, Till Mossakowski, Florian Rabe

In: Narciso Martí-Oliet , Miguel Palomino (Hrsg.). Proceedings of the 21st International Workshop on Algebraic Development Techniques. International Workshop on Algebraic Development Techniques (WADT-12) Recent Trends in Algebraic Development Techniques June 7-10 Salamanca Spain Seiten 111-126 Lecture Notes in Computer Science (LNCS) 7841 Springer 2013.


We present an architecture that permits compiling declarative logic specifications (given in some type theory like LF) into implementations of that logic within the Heterogeneous Tool Set Hets. The central contributions are the use of declaration patterns for singling out a suitable subset of signatures for a particular logic, and the automatic generation of datatypes and functions for parsing and static analysis of declaratively specified logics

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence