Rewritings in Polarized (Partial) Proof Structures
type: Distribution
access URL: https://hal.science/hal-00084354
format: HTML
issued: 2026-05-10T09:31:22.322607
modified: 2026-05-10T09:31:22.313661

test_moissonnage_selune
type: Agent

Rewritings in Polarized (Partial) Proof Structures
type: Dataset
contact point: Organization
  fn: CCSD
keyword: infoinfo-locomputer-science-cslogic-in-computer-science-cslo
keyword: conference-papers
keyword: mathmath-lomathematics-mathlogic-mathlo
keyword: infoinfo-dccomputer-science-csdistributed-parallel-and-cluster-computing-csdc
keyword: infoeu-reposemanticsconferenceobject
landing page: Structures and Deduction - the Quest for the Essence of Proofs ICALP Workshop
description: 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.
issued: 2026-05-10T09:31:22.320481
language: en
modified: 2026-05-10T09:31:22.320485