article

Open access

Simplification by Cooperating Decision Procedures

Editor: Susan L. Graham Authors:

Greg Nelson,

Derek C. OppenAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 1, Issue 2

Pages 245 - 257

https://doi.org/10.1145/357073.357079

Published: 01 October 1979 Publication History

PDF eReader

Abstract

A method for combining decision procedures for several theories into a single decision procedure for their combination is described, and a simplifier based on this method is discussed. The simplifier finds a normal form for any expression formed from individual variables, the usual Boolean connectives, the equality predicate =, the conditional function if-then-else, the integers, the arithmetic functions and predicates +, -, and ≤, the Lisp functions and predicates car, cdr, cons, and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. If the expression is a theorem it is simplified to the constant true, so the simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier.

References

[1]

CRAIG, W. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22 (1955).

Google Scholar

[2]

DOWNEY, P.J., AND SETm, R. Assignment commands with array references. J. ACM 25, 4 (Oct. 1978), 652-666.

Crossref

Google Scholar

[3]

DOWNEY, P., SETHL R., AND TARZAN, R. Variations on the common subexpression problem. To appear in J. A CM.

Crossref

Google Scholar

[4]

KAPLAN, D.M. Some completeness results in the mathematical theory of computation. J. ACM 15, I (Jan. 1968), 124-134.

Crossref

Google Scholar

[5]

MATIYASEVlCH, Y.V. Diophantine representation ofrecursively enumerable predicates. Proc. 2nd Scandinavian Logic Symposium, North-Holland Publ. Co., 1970.

Google Scholar

[6]

MCCARTHY, J. A basis for a mathematical theory of computation. In Computing Programming and Formal Systems, P. Braffort and D. Hirshberg, Eds. North-Holland Publ. Co., 1963.

Google Scholar

[7]

NELSON, C.G., AND OFTEN, D.C. Fast decision algorithms based on congruence closure. CS Rep. STAN-CS-77-646, Stanford U., 1978.

Crossref

Google Scholar

[8]

OPPEN, D.C. Convexity, complexity, and combinations of theories. To appear in Theoretical Comptr. Sci.

Google Scholar

[9]

OFTEN, D.C. Reasoning about recursively defined data structures. To appear in J. ACM.

Crossref

Google Scholar

[10]

SCHOENFIELD, J.R. Mathematical Logic. Addison-Wesley, Reading, Mass., 1967.

Google Scholar

[11]

SHOSTAK, R.E. An practical decision procedure for arithmetic with function symbols. J. ACM26, 2 (April 1979), 351-360.

Crossref

Google Scholar

[12]

SuzuKI, N., AND JEFFERSON, D. Verification decidability of Presburger array programs. Proc. Conf. on Theoretical Computer Science, U. of Waterloo, Aug. 1977.

Google Scholar

[13]

TAKEUC}II, I. Private communication to J. McCarthy.

Google Scholar

[14]

TARSKI, A. A decision method for elementary algebra and geometry. Berkeley, 1951.

Google Scholar

Cited By

View all

Mathur UMestel DViswanathan M(2025)The Decision Problem for Regular First Order TheoriesProceedings of the ACM on Programming Languages10.1145/37048709:POPL(986-1012)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704870
Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656450
Hague MJeż ALin A(2024)Parikh’s Theorem Made SymbolicProceedings of the ACM on Programming Languages10.1145/36329078:POPL(1945-1977)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632907
Show More Cited By

Index Terms

Simplification by Cooperating Decision Procedures

Recommendations

Simplification by cooperating decision procedures
Safraless Decision Procedures
FOCS '05: Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science

The automata-theoretic approach is one of the most fundamental approaches to developing decision procedures in mathematical logics. To decide whether a formula in a logic with the tree-model property is satisfiable, one constructs an automaton that ...
Verified decision procedures for MSO on words based on derivatives of regular expressions
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Monadic second-order logic on finite words (MSO) is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced to the equivalence of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 1, Issue 2

Oct. 1979

160 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/357073

Editor:
Susan L. Graham

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 1979

Published in TOPLAS Volume 1, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

687
Total Citations
View Citations
2,634
Total Downloads

Downloads (Last 12 months)351
Downloads (Last 6 weeks)64

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Mathur UMestel DViswanathan M(2025)The Decision Problem for Regular First Order TheoriesProceedings of the ACM on Programming Languages10.1145/37048709:POPL(986-1012)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704870
Murali ARivera CMadhusudan P(2024)Predictable Verification using Intrinsic DefinitionsProceedings of the ACM on Programming Languages10.1145/36564508:PLDI(1804-1829)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656450
Hague MJeż ALin A(2024)Parikh’s Theorem Made SymbolicProceedings of the ACM on Programming Languages10.1145/36329078:POPL(1945-1977)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632907
Raya RKunčak V(2024)Succinct ordering and aggregation constraints in algebraic array theoriesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100978140(100978)Online publication date: Aug-2024
https://doi.org/10.1016/j.jlamp.2024.100978
Ringeissen CVigneron L(2024)Combined Abstract Congruence Closure for Theories with Associativity or CommutativityLogic-Based Program Synthesis and Transformation10.1007/978-3-031-71294-4_5(82-98)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71294-4_5
Przybocki BToledo GZohar YBarrett C(2024)The Nonexistence of Unicorns and Many-Sorted Löwenheim–Skolem TheoremsFormal Methods10.1007/978-3-031-71162-6_34(658-675)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_34
Sun YJi RFang JJiang XChen MXiong Y(2024)Proving Functional Program Equivalence via Directed Lemma SynthesisFormal Methods10.1007/978-3-031-71162-6_28(538-557)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_28
Sutcliffe GSuttner CKotthoff LPerrault CKhalid Z(2024)An Empirical Assessment of Progress in Automated Theorem ProvingAutomated Reasoning10.1007/978-3-031-63498-7_4(53-74)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_4
Seidl HErhard JSchwarz MTilscher S(2024)2-Pointer LogicTaming the Infinities of Concurrency10.1007/978-3-031-56222-8_16(281-307)Online publication date: 20-Mar-2024
https://doi.org/10.1007/978-3-031-56222-8_16
Diaconescu R(2023)Concepts of Interpolation in Stratified InstitutionsLogics10.3390/logics10200051:2(80-96)Online publication date: 3-Apr-2023
https://doi.org/10.3390/logics1020005
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations