Rewritings in Polarized (Partial) Proof Structures

This paper is a first step towards a study for a concurrent construction of proof-nets in the framework of linear logic after Andreoli's works, by taking care of the properties of the structures. We limit here to multiplicative linear logic. We first give a criterion for closed modules (i.e. validity of polarized proof structures), then extend it to open modules (i.e. validity of partial proof structures) distinguishing criteria for acyclicity and connectability. The keypoint is an extensive use of the fundamental structural properties of the logics. We consider proof structures as built from n-ary bipolar objects and we show that strongly confluent (local) reductions on such objects are an elegant answer to the correctness problem. This has natural applications in (concurrent) logic programming.

Data and Resources

Additional Info

Field Value
Source Structures and Deduction - the Quest for the Essence of Proofs ICALP Workshop
Author Fouqueré, Christophe, Mogbil, Virgile
Maintainer CCSD
Last Updated May 10, 2026, 09:31 (UTC)
Created May 10, 2026, 09:31 (UTC)
Identifier hal-00084354
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Laboratoire d'Informatique de Paris-Nord (LIPN) ; Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS)
coverage Lisbon, Portugal
creator Fouqueré, Christophe
date 2005-07-16T00:00:00
harvest_object_id 33082665-5ada-4f99-8b18-bc25830c4abd
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2024-11-28T00:00:00
set_spec type:COMM