Focussing and proof construction
type: Item
instance of: scholarly article
title: Focussing and proof construction
zbMATH Open document ID: 0966.03053
DOI: 10.1016/S0168-0072(00)00032-4
author: Jean-Marc Andreoli
published in: Annals of Pure and Applied Logic
publication date: 2001-07-24T00:00:00Z
review text: The foundation of the proof-construction paradigm and its central feature: non-determinism and partial information in logic programming, are discussed. A new presentation of the focussing proof system for linear logic is given. A new presentation of the ``normal form'' for linear logic, and in particular the notions of bipolarisation and universal program are introduced. A new, constraint-based approach to the proof-construction paradigm, illustrating another of its essential features: the capacity to deal with partial information, is presented.
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 68N17
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 1562994
zbMATH Keywords: linear logic
zbMATH Keywords: proof construction
zbMATH Keywords: focusing proofs
zbMATH Keywords: constraint propagation
zbMATH Keywords: tableau methods
describes a project that uses: Lolli
MaRDI profile type: Publication
cites work: Logic Programming with Focusing Proofs in Linear Logic
cites work: True concurrency semantics for a linear logic programming language with broadcast communication
cites work: Linear logic
cites work: Light linear logic
cites work: Resource-distribution via Boolean constraints
cites work: Logic programming in a fragment of intuitionistic linear logic
cites work: Uniform proofs as a foundation for logic programming
description: scientific article; zbMATH DE number 1562994