Please use this identifier to cite or link to this item:
doi:10.22028/D291-41469
Title: | A Colored Version of the lambda-Calculus |
Author(s): | Hutter, Dieter Kohlhase, Michael |
Language: | English |
Year of Publication: | 1995 |
Place of publication: | Saarbrücken |
DDC notations: | 004 Computer science, internet |
Publikation type: | Report |
Abstract: | Coloring terms (rippling) is a technique developed for inductive theorem proving which uses syntactic differences of terms to guide the proof search. Annotations (colors) to terms are used to maintain this information. This technique has several advantages, e.g. it is highly goal oriented and involves little search. In this paper we give a general formalization of coloring terms in a higher-order setting. We introduce a simply-typed lambda calculus with color annotations and present an appropriate (pre-)unification algorithm. Our work is a formal basis to the implementation of rippling in a higher-order setting which is required e.g. in case of middle-out reasoning. Another application is in the construction of natural language semantics, where the color annotations rule out linguistically invalid readings that are possible using standard higher-order unification. |
Link to this record: | urn:nbn:de:bsz:291--ds-414690 hdl:20.500.11880/37778 http://dx.doi.org/10.22028/D291-41469 |
Series name: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Series volume: | 95,5 |
Date of registration: | 4-Jun-2024 |
Faculty: | SE - Sonstige Einrichtungen |
Department: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Professorship: | SE - Sonstige |
Collections: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Files for this record:
File | Description | Size | Format | |
---|---|---|---|---|
SEKI-Report-SR-95-05_Hutter-Kohlhase_A-Colored-Version-of-the-[lambda]=Calculus.pdf | 4,15 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.