We present a congruence relation on sequent-style classical proofs which identifies proofs up to trivial rule permutation. The study is performed in the framework of the ∗X calculus, which provides a Curry–Howard correspondence for classical logic (with explicit structural rules), ensuring that proofs can be seen as terms and proof transformations as computations. Congruence equations provide an explicit account for classifying proofs (terms) that are syntactically different but essentially the same. We prove that there is always a representative of a congruence class that enables computation at the top level.
A Congruence Relation for Restructuring Classical Terms
Zunic, Dragisa
2018-01-01
Abstract
We present a congruence relation on sequent-style classical proofs which identifies proofs up to trivial rule permutation. The study is performed in the framework of the ∗X calculus, which provides a Curry–Howard correspondence for classical logic (with explicit structural rules), ensuring that proofs can be seen as terms and proof transformations as computations. Congruence equations provide an explicit account for classifying proofs (terms) that are syntactically different but essentially the same. We prove that there is always a representative of a congruence class that enables computation at the top level.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.
