scientific article; zbMATH DE number 2247255
From MaRDI portal
Publication:5718567
zbMath1096.03068MaRDI QIDQ5718567
Ulrich Berger, Monika Seisenberger
Publication date: 16 January 2006
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Higman's lemmainductive definitionsinfinite sequencesextracting constructive content from classical proofsinteractive proof system Minlognonconstructive choice principlesproof-theoretic optimizations
Mechanization of proofs and logical operations (03B35) Other constructive mathematics (03F65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Proof theory in general (including proof-theoretic semantics) (03F03)
Related Items (2)
Programs from proofs using classical dependent choice ⋮ From Coinductive Proofs to Exact Real Arithmetic
This page was built for publication:
