Decision procedures for term algebras with integer constraints

DOI10.1016/J.IC.2006.03.004MaRDI QIDQ2432767zbMATHOpenAlexFDO

Authors Ting Zhang, Zohar Manna, Henny B. Sipma

Publication date 25 October 2006

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2006.03.004

zbMATH Keywords

decision proceduresquantifier eliminationPresburger arithmeticrecursive data structurescombination of satisfiability proceduresterm algebras

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Quantifier elimination, model completeness, and related topics (03C10)

Recommendations

• Automated Reasoning
• A decision procedure for term algebras with queues
• Theorem Proving in Higher Order Logics
• Decision procedures for algebraic data types with abstractions
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science

Cites work

• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 53151 (Why is no real title available?)
• scientific article; zbMATH DE number 3478862 (Why is no real title available?)
• scientific article; zbMATH DE number 3577484 (Why is no real title available?)
• scientific article; zbMATH DE number 487720 (Why is no real title available?)
• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• scientific article; zbMATH DE number 1754649 (Why is no real title available?)
• scientific article; zbMATH DE number 2086594 (Why is no real title available?)
• scientific article; zbMATH DE number 1848313 (Why is no real title available?)
• scientific article; zbMATH DE number 2090313 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• A complete axiomatization of a theory with feature and arity constraints
• A decision procedure for term algebras with queues
• A mathematical introduction to logic.
• Advances in Databases and Information Systems
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Automated Reasoning
• Equational formulae with membership constraints
• Equational problems and disunification
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Fast Decision Procedures Based on Congruence Closure
• Logics in Artificial Intelligence
• Model-theoretic methods in combined constraint satisfiability
• Presburger arithmetic with bounded quantifier alternation
• Reasoning About Recursively Defined Data Structures
• Simplification by Cooperating Decision Procedures
• The first order properties of products of algebraic systems
• Theorem Proving in Higher Order Logics
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Variations on the Common Subexpression Problem
• Verification, Model Checking, and Abstract Interpretation

Cited in

(10)

• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• A rewriting approach to the combination of data structures with bridging theories
• Coming to terms with quantified reasoning
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Politeness and combination methods for theories with bridging functions
• Automated Reasoning
• Quantitative separation logic and programs with lists
• A decision procedure for term algebras with queues
• A polite non-disjoint combination method: theories with bridging functions revisited
• Theorem Proving in Higher Order Logics

This page was built for publication: Decision procedures for term algebras with integer constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2432767)