On the SUP-INF Method for Proving Presburger Formulas
From MaRDI portal
Publication:3857732
DOI10.1145/322033.322034zbMath0423.68052OpenAlexW1996325171MaRDI QIDQ3857732
Publication date: 1977
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322033.322034
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (13)
Conditional rewrite rule systems with built-in arithmetic and induction ⋮ A structure-preserving clause form translation ⋮ A multi-level geometric reasoning system for vision ⋮ From LP to LP: Programming with constraints ⋮ Symbolic reasoning among 3-D models and 2-D images ⋮ SLAP: specification logic of actions with probability ⋮ Problem-oriented program verification system ?SPEKTR? ⋮ The two variable per inequality abstract domain ⋮ A canonical form for generalized linear constraints ⋮ A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure ⋮ The complexity of almost linear diophantine problems ⋮ Problem-oriented verification system and its application to linear algebra programs ⋮ Symbolic model checking of timed guarded commands using difference decision diagrams
This page was built for publication: On the SUP-INF Method for Proving Presburger Formulas
