A Practical Decision Procedure for Arithmetic with Function Symbols
From MaRDI portal
Publication:3960818
DOI10.1145/322123.322137zbMath0496.03003OpenAlexW1988192943MaRDI QIDQ3960818
Publication date: 1979
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322123.322137
program verificationextension of quantifier-free Presburger arithmetic that permits arbitrary uninterpreted predicate and function symbolssemantics of array operators
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)
Related Items
An overview of the Tecton proof system ⋮ Conditional rewrite rule systems with built-in arithmetic and induction ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Combination of constraint solvers for free and quasi-free structures ⋮ Complexity, convexity and combinations of theories ⋮ Spectra and satisfiability for logics with successor and a unary function ⋮ Decidable cases of first-order temporal logic with functions ⋮ A taxonomy of exact methods for partial Max-SAT ⋮ Problem-oriented program verification system ?SPEKTR? ⋮ Properties of a predicate transformer of the VRS system ⋮ Predicate transformers in the context of symbolic modeling of transition systems ⋮ Elimination Techniques for Program Analysis ⋮ Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ Str∔ve and integers ⋮ Politeness and combination methods for theories with bridging functions ⋮ Colors Make Theories Hard ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Polite combination of algebraic datatypes ⋮ Politeness for the theory of algebraic datatypes ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I
