算術で方程式を証明する

プレスバーガー(Presburger)算術の方程式バージョンについての公理を指定する．

プレスバーガー算術で二重否定の定理を証明する．

完全な証明における補題のリストを表示する．