Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
A Conditional Logical Framework
verfasst von : Furio Honsell, Marina Lenisa, Luigi Liquori, Ivan Scagnetto
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The
Conditional Logical Framework
LF
K
is a variant of the Harper-Honsell-Plotkin’s Edinburgh Logical Framemork
LF
. It features a generalized form of
λ
-abstraction where
β
-reductions fire
under the condition
that the argument satisfies a
logical predicate
. The key idea is that the type system
memorizes
under what conditions and where reductions have yet to fire. Different notions of
β
-reductions corresponding to different predicates can be combined in
LF
K
. The framework
LF
K
subsumes, by simple instantiation,
LF
(in fact, it is also a subsystem of
LF
!), as well as a large class of new generalized conditional
λ
-calculi. These are appropriate to deal smoothly with the side-conditions of both Hilbert and Natural Deduction presentations of Modal Logics. We investigate and characterize the metatheoretical properties of the calculus underpinning
LF
K
, such as subject reduction, confluence, strong normalization.