Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Construction of Retractile Proof Structures
verfasst von : Roberto Maieli
Erschienen in: Rewriting and Typed Lambda Calculi
Verlag: Springer International Publishing
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
In this work we present a paradigm of focusing proof search based on an incremental construction of
retractile
(i.e,
correct
or
sequentializable
) proof structures of the pure (units free) multiplicative and additive fragment of linear logic. The correctness of proof construction steps (or expansion steps) is ensured by means of a system of graph retraction rules; this graph rewriting system is shown to be convergent, that is, terminating and confluent. Moreover, the proposed proof construction follows an optimal (parsimonious, indeed) retraction strategy that, at each expansion step, allows to take into account (abstract) graphs that are ”smaller” (w.r.t. the size) than the starting proof structures.