Decision procedures for term algebras with integer constraints

DOI10.1016/J.IC.2006.03.004MaRDI QIDQ2432767zbMATH OpenOpenAlexFDO

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

combination of satisfiability proceduresdecision proceduresPresburger arithmeticquantifier eliminationrecursive data structuresterm algebras

Mathematics Subject Classification ID

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) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60)

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

• 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
• Fast Decision Procedures Based on Congruence Closure
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• 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?)
• 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)

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

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)