Reasoning About Recursively Defined Data Structures
From MaRDI portal
Cited in
(24)- A view of computability on term algebras
- An algebraic semantics approach to the effective resolution of type equations
- Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
- On the relationship of congruence closure and unification
- Complexity, convexity and combinations of theories
- Inferring the equivalence of functional programs that mutate data
- Embedding complex decision procedures inside an interactive theorem prover.
- Reasoning about algebraic data types with abstractions
- Quantifier elimination for infinite terms
- Politeness and combination methods for theories with bridging functions
- Unification modulo lists with reverse relation with certain word equations
- Decision procedures for term algebras with integer constraints
- Colors Make Theories Hard
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Rewrite-based satisfiability procedures for recursive data structures
- Quantifier Elimination and Provers Integration
- Equivalence in functional languages with effects
- scientific article; zbMATH DE number 7453200 (Why is no real title available?)
- Locality Results for Certain Extensions of Theories with Bridging Functions
- Quantifier-free interpolation in combinations of equality interpolating theories
- Automatic decidability and combinability
- Model-theoretic methods in combined constraint satisfiability
- Solving constrained Horn clauses over algebraic data types
- Relatively complete and efficient partial quantifier elimination
This page was built for publication: Reasoning About Recursively Defined Data Structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3935457)
