Classical computation with negation
Dragiša Žunić, Pierre Lescanne · AIP conference proceedings · 2012
We study the computational content of negation in classical logic. This is done in the framework of *K calculus, which has been designed to stand in correspondence with classical logic with explicit structural rules. The terms for left-negation and right-negation are introduced and their computational role is defined by reduction rules. We show that good underlying properties of the original system are preserved in the system extended with negations.