The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction

DOI10.1023/A:1026748613865zbMath0958.03009OpenAlexW1772256284MaRDI QIDQ1595930

Ulrich Berger, Helmut Schwichtenberg, Monika Seisenberger

Publication date: 18 February 2001

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1026748613865

zbMATH Keywords

Dickson's lemmarealizabilityprogram extractionconstructive proofsA-translationprovably correct programsWarshall algorithm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (8)

Getting results from programs extracted from classical proofs ⋮ Extracting a DPLL Algorithm ⋮ Mathematical method and proof ⋮ Proof-theoretic notions for software maintenance ⋮ Refined program extraction from classical proofs ⋮ The metamathematics of ergodic theory ⋮ Decision procedure of some relevant logics: a constructive perspective ⋮ Light Dialectica Program Extraction from a Classical Fibonacci Proof

Uses Software

• Minlog

This page was built for publication: The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction