Decision procedures for term algebras with integer constraints

DOI10.1016/J.IC.2006.03.004zbMATH Open1103.68080OpenAlexW4206132523MaRDI QIDQ2432767FDOQ2432767

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

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

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)

Cites Work

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

Cited In (10)

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

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)