Variant-Based Satisfiability in Initial Algebras
From MaRDI portal
Publication:4686604
Recommendations
- Variant-based decidable satisfiability in initial algebras with predicates
- Metalevel algorithms for variant satisfiability
- Metalevel algorithms for variant satisfiability
- Variants and satisfiability in the infinitary unification wonderland
- Theory and Applications of Satisfiability Testing
- Variant Satisfiability of Parameterized Strings
- On Some SAT-Variants over Linear Formulas
- Publication:4729350
- scientific article; zbMATH DE number 1222558
- On variable-weighted exact satisfiability problems
Cites work
- scientific article; zbMATH DE number 1688811 (Why is no real title available?)
- scientific article; zbMATH DE number 4018380 (Why is no real title available?)
- scientific article; zbMATH DE number 3888893 (Why is no real title available?)
- scientific article; zbMATH DE number 3817070 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 1337735 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1765694 (Why is no real title available?)
- scientific article; zbMATH DE number 1765696 (Why is no real title available?)
- scientific article; zbMATH DE number 1798183 (Why is no real title available?)
- scientific article; zbMATH DE number 1903346 (Why is no real title available?)
- scientific article; zbMATH DE number 1903356 (Why is no real title available?)
- scientific article; zbMATH DE number 2090300 (Why is no real title available?)
- scientific article; zbMATH DE number 5194318 (Why is no real title available?)
- scientific article; zbMATH DE number 3289430 (Why is no real title available?)
- A proof theory for general unification
- A rewriting approach to satisfiability procedures.
- A uniform approach to constraint-solving for lists, multisets, compact lists, and sets
- Adding decision procedures to SMT solvers using axioms with triggers
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- An abstract decision procedure for a theory of inductive data types.
- An instantiation scheme for satisfiability modulo theories
- Asymmetric unification: a new unification paradigm for cryptographic protocol analysis
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Automated complexity analysis based on ordered resolution
- Automated verification of equivalence properties of cryptographic protocols
- Automatic Decidability and Combinability Revisited
- Combination techniques and decision problems for disunification
- Combined Satisfiability Modulo Parametric Theories
- Combining unification algorithms
- Complete axiomatizations of some quotient term algebras
- Complete sets of transformations for general E-unification
- Completion of a Set of Rules Modulo a Set of Equations
- Complexity of unification problems with associative-commutative operators
- Complexity, convexity and combinations of theories
- Counterexamples to termination for the direct sum of term rewriting systems
- Deciding Combinations of Theories
- Deciding inductive validity of equations.
- Equational formulae with membership constraints
- Equational formulas and pattern operations in initial order-sorted algebras
- Equational problems and disunification
- Fast Decision Procedures Based on Congruence Closure
- Folding Variant Narrowing and Optimal Variant Termination
- Folding variant narrowing and optimal variant termination
- Infinite-state model checking of LTLR formulas using narrowing
- Institutions: abstract model theory for specification and programming
- Logics in Artificial Intelligence
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Mechanizing Mathematical Reasoning
- Modular termination of basic narrowing and equational unification
- Modularity in term rewriting revisited
- New results on rewrite-based satisfiability procedures
- On Forward Closure and the Finite Variant Property
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- Order-Sorted Parameterization and Induction
- Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Simplification by Cooperating Decision Procedures
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Strict coherence of conditional rewriting modulo axioms
- Term Rewriting and Applications
- Term Rewriting and Applications
- Termination of narrowing revisited
- Theorem proving using lazy proof explication.
- Theoretical Aspects of Computing – ICTAC 2005
- Unification in the union of disjoint equational theories: Combining decision procedures
Cited in
(25)- Optimization of rewrite theories by equational partial evaluation
- On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
- An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
- Variant Satisfiability of Parameterized Strings
- Built-in variant generation and unification, and their applications in Maude 2.7
- Symbolic Specialization of Rewriting Logic Theories with Presto
- Non-disjoint combined unification and closure by equational paramodulation
- Programming and symbolic computation in Maude
- Checking Sufficient Completeness by Inductive Theorem Proving
- Variants and satisfiability in the infinitary unification wonderland
- A partial evaluation framework for order-sorted equational programs modulo axioms
- Ground confluence of order-sorted conditional specifications modulo axioms
- Equational formulas and pattern operations in initial order-sorted algebras
- Optimizing Maude programs via program specialization
- Metalevel algorithms for variant satisfiability
- Metalevel algorithms for variant satisfiability
- Politeness for the theory of algebraic datatypes
- Generalized rewrite theories, coherence completion, and symbolic methods
- Symbolic computation in Maude: some tapas
- scientific article; zbMATH DE number 7453112 (Why is no real title available?)
- scientific article; zbMATH DE number 7455704 (Why is no real title available?)
- Terminating non-disjoint combined unification
- Variant-based decidable satisfiability in initial algebras with predicates
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- Polite combination of algebraic datatypes
This page was built for publication: Variant-Based Satisfiability in Initial Algebras
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4686604)
