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. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Maieli, R. (2014). Construction of retractile proof structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 319–333). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_22
Mendeley helps you to discover research relevant for your work.