We propose a new direct presentation of full (propositional) classical logic by means of proof nets, for which strong normalization and confluence hold true. Our proposal is based on the breaking of symmetry between propositional connectives, combined with a principle of focusing/defocusing.

Proof Nets for Classical Logic

Masini, Andrea
2021-01-01

Abstract

We propose a new direct presentation of full (propositional) classical logic by means of proof nets, for which strong normalization and confluence hold true. Our proposal is based on the breaking of symmetry between propositional connectives, combined with a principle of focusing/defocusing.
2021
proof theory, proof nets, classical logic
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1044766
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact