A procedure for automatic proof nets construction | Zendy

Didier Galmiche | Zendy; Guy Perrier | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A procedure for automatic proof nets construction

Author(s) -

Didier Galmiche,

Guy Perrier

Publication year - 2005

Publication title -

logic programming and automated reasoning

Language(s) - English

Resource type - Book series

ISBN - 3-540-55727-X

DOI - 10.1007/bfb0013047

Subject(s) - linear logic , correctness , mathematical proof , sequent calculus , sequent , computer science , natural deduction , proof calculus , proof theory , programming language , completeness (order theory) , structural proof theory , curry–howard correspondence , construct (python library) , algorithm , theoretical computer science , mathematics , mathematical analysis , geometry

. In this paper, we consider the multiplicative fragment of linearlogic (MLL) from an automated deduction point of view. Before to use thisnew logic to make logic programming or to program with proofs, a bettercomprehension of the proof construction process in this framework is necessary.We propose a new algorithm to construct automatically a proof netfor a given sequent in MLL and its proofs of termination, correctness andcompleteness. It can be seen as an implementation oriented way to...

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research