Sciweavers

CADE
1992
Springer
14 years 4 months ago
Isabelle-91
e introducing the types and constants of the logic, i.e. its abstract syntax, and axioms describing the inference rules. As a tiny example, consider the following definition of min...
Tobias Nipkow, Lawrence C. Paulson
CIE
2010
Springer
14 years 5 months ago
The Peirce Translation and the Double Negation Shift
We develop applications of selection functions to proof theory and computational extraction of witnesses from proofs in classical analysis. The main novelty is a translation of cla...
Martín Hötzel Escardó, Paulo Ol...